equal
deleted
inserted
replaced
7 theory Orderings |
7 theory Orderings |
8 imports HOL |
8 imports HOL |
9 keywords "print_orders" :: diag |
9 keywords "print_orders" :: diag |
10 begin |
10 begin |
11 |
11 |
12 ML_file "~~/src/Provers/order.ML" |
12 ML_file \<open>~~/src/Provers/order.ML\<close> |
13 ML_file "~~/src/Provers/quasi.ML" (* FIXME unused? *) |
13 ML_file \<open>~~/src/Provers/quasi.ML\<close> (* FIXME unused? *) |
14 |
14 |
15 subsection \<open>Abstract ordering\<close> |
15 subsection \<open>Abstract ordering\<close> |
16 |
16 |
17 locale ordering = |
17 locale ordering = |
18 fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^bold>\<le>" 50) |
18 fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^bold>\<le>" 50) |