--- a/NEWS Fri Jan 13 01:13:17 2006 +0100
+++ b/NEWS Fri Jan 13 14:43:09 2006 +0100
@@ -216,6 +216,11 @@
* Provers/induct: support coinduction as well. See
src/HOL/Library/Coinductive_List.thy for various examples.
+* Simplifier: by default the simplifier trace only shows top level rewrites
+now. That is, trace_simp_depth_limit is set to 1 by default. Thus there is
+less danger of being flooded by the trace. The trace indicates where parts
+have been suppressed.
+
* Provers/classical: removed obsolete classical version of elim_format
attribute; classical elim/dest rules are now treated uniformly when
manipulating the claset.
@@ -241,6 +246,8 @@
25 like -->); output depends on the "iff" print_mode, the default is
"A = B" (with priority 50).
+* "LEAST x:A. P" expands to "LEAST x. x:A & P" (input only).
+
* In the context of the assumption "~(s = t)" the Simplifier rewrites
"t = s" to False (by simproc "neq_simproc"). For backward
compatibility this can be disabled by ML "reset use_neq_simproc".
--- a/src/HOL/Set.thy Fri Jan 13 01:13:17 2006 +0100
+++ b/src/HOL/Set.thy Fri Jan 13 14:43:09 2006 +0100
@@ -64,6 +64,8 @@
"_Ball" :: "pttrn => 'a set => bool => bool" ("(3ALL _:_./ _)" [0, 0, 10] 10)
"_Bex" :: "pttrn => 'a set => bool => bool" ("(3EX _:_./ _)" [0, 0, 10] 10)
+ "_Bleast" :: "id => 'a set => bool => 'a" ("(3LEAST _:_./ _)" [0, 0, 10] 10)
+
syntax (HOL)
"_Ball" :: "pttrn => 'a set => bool => bool" ("(3! _:_./ _)" [0, 0, 10] 10)
@@ -86,6 +88,8 @@
"INT x:A. B" == "INTER A (%x. B)"
"ALL x:A. P" == "Ball A (%x. P)"
"EX x:A. P" == "Bex A (%x. P)"
+ "LEAST x:A. P" => "LEAST x. x:A & P"
+
syntax (output)
"_setle" :: "'a set => 'a set => bool" ("op <=")
@@ -108,6 +112,7 @@
Inter :: "'a set set => 'a set" ("\<Inter>_" [90] 90)
"_Ball" :: "pttrn => 'a set => bool => bool" ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
"_Bex" :: "pttrn => 'a set => bool => bool" ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
+ "_Bleast" :: "id => 'a set => bool => 'a" ("(3LEAST_\<in>_./ _)" [0, 0, 10] 10)
syntax (HTML output)
"_setle" :: "'a set => 'a set => bool" ("op \<subseteq>")