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.
definition less_int_def has changed, use 'less_le' instead
authorhuffman
Thu, 31 May 2012 15:47:06 +0200
changeset 48050 72acba14c12b
parent 48049 d862b0d56c49
child 48054 60bcc6cf17d6
definition less_int_def has changed, use 'less_le' instead
src/HOL/Metis_Examples/Sets.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Metis_Examples/Sets.thy	Mon May 28 02:18:46 2012 +0200
+++ b/src/HOL/Metis_Examples/Sets.thy	Thu May 31 15:47:06 2012 +0200
@@ -195,7 +195,7 @@
        apply (metis all_not_in_conv)
       apply (metis all_not_in_conv)
      apply (metis mem_Collect_eq)
-    apply (metis less_int_def singleton_iff)
+    apply (metis less_le singleton_iff)
    apply (metis mem_Collect_eq)
   apply (metis mem_Collect_eq)
  apply (metis all_not_in_conv)
isabelle