equal
deleted
inserted
replaced
5 header {* Abstract orderings *} |
5 header {* Abstract orderings *} |
6 |
6 |
7 theory Orderings |
7 theory Orderings |
8 imports HOL |
8 imports HOL |
9 keywords "print_orders" :: diag |
9 keywords "print_orders" :: diag |
10 uses |
10 begin |
11 "~~/src/Provers/order.ML" |
11 |
12 "~~/src/Provers/quasi.ML" (* FIXME unused? *) |
12 ML_file "~~/src/Provers/order.ML" |
13 begin |
13 ML_file "~~/src/Provers/quasi.ML" (* FIXME unused? *) |
14 |
14 |
15 subsection {* Syntactic orders *} |
15 subsection {* Syntactic orders *} |
16 |
16 |
17 class ord = |
17 class ord = |
18 fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
18 fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |