Skip to content

Commit 1bd63d0

Browse files
Casteranpalmskog
andauthored
Update theories/ordinals/OrdinalNotations/ON_Omega_plus_omega.v
Co-authored-by: Karl Palmskog <palmskog@gmail.com>
1 parent 4cb9ca1 commit 1bd63d0

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

theories/ordinals/OrdinalNotations/ON_Omega_plus_omega.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -398,7 +398,7 @@ Lemma Omega_as_lub :
398398

399399
(* begin snippet Incl *)
400400

401-
#[ global] Instance Incl : SubON Omega Omega_plus_Omega omega fin. (* .no-out *)
401+
#[global] Instance Incl : SubON Omega Omega_plus_Omega omega fin. (* .no-out *)
402402

403403
(* end snippet Incl *)
404404
Proof.

0 commit comments

Comments
 (0)