equal
deleted
inserted
replaced
7 |
7 |
8 section \<open>Constructions on Wellorders\<close> |
8 section \<open>Constructions on Wellorders\<close> |
9 |
9 |
10 theory Wellorder_Constructions |
10 theory Wellorder_Constructions |
11 imports |
11 imports |
12 BNF_Wellorder_Constructions Wellorder_Embedding Order_Union |
12 HOL.BNF_Wellorder_Constructions Wellorder_Embedding Order_Union |
13 "../Library/Cardinal_Notations" |
13 "HOL-Library.Cardinal_Notations" |
14 begin |
14 begin |
15 |
15 |
16 declare |
16 declare |
17 ordLeq_Well_order_simp[simp] |
17 ordLeq_Well_order_simp[simp] |
18 not_ordLeq_iff_ordLess[simp] |
18 not_ordLeq_iff_ordLess[simp] |