equal
deleted
inserted
replaced
55 lemma antisym_conv: "y \<le> x \<Longrightarrow> x \<le> y \<longleftrightarrow> x \<approx> y" |
55 lemma antisym_conv: "y \<le> x \<Longrightarrow> x \<le> y \<longleftrightarrow> x \<approx> y" |
56 by (simp add: equiv_def) |
56 by (simp add: equiv_def) |
57 |
57 |
58 end |
58 end |
59 |
59 |
60 thm order_trans |
|
61 |
|
62 find_theorems "?i < ?j \<Longrightarrow> ?i \<le> ?j" |
|
63 |
|
64 ML_file \<open>~~/src/Provers/preorder.ML\<close> |
60 ML_file \<open>~~/src/Provers/preorder.ML\<close> |
65 |
61 |
66 ML \<open> |
62 ML \<open> |
67 structure Quasi = Quasi_Tac( |
63 structure Quasi = Quasi_Tac( |
68 struct |
64 struct |