Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Unknown change.
authorballarin
Wed, 30 Apr 2003 18:33:41 +0200
changeset 13941 2ae108fcd068
parent 13940 c67798653056
child 13942 dc93e3a68142
Unknown change.
src/Provers/linorder.ML file | annotate | diff | comparison | revisions 
--- a/src/Provers/linorder.ML	Wed Apr 30 18:32:06 2003 +0200
+++ b/src/Provers/linorder.ML	Wed Apr 30 18:33:41 2003 +0200
@@ -40,7 +40,7 @@
 sig
   val less_reflE: thm  (* x < x ==> P *)
   val le_refl: thm  (* x <= x *)
-  val less_imp_le: thm (* x <= y ==> x < y *)
+  val less_imp_le: thm (* x < y ==> x <= y *)
   val not_lessI: thm (* y <= x  ==> ~(x < y) *)
   val not_leI: thm (* y < x  ==> ~(x <= y) *)
   val not_lessD: thm (* ~(x < y) ==> y <= x *)
isabelle