# HG changeset patch
# User huffman
# Date 1338472026 -7200
# Node ID 72acba14c12bab6359b7650d22e71d6a7dde9079
# Parent  d862b0d56c49d9ba72b51559af98f11b92e83164
definition less_int_def has changed, use 'less_le' instead

diff -r d862b0d56c49 -r 72acba14c12b src/HOL/Metis_Examples/Sets.thy
--- 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)