*** empty log message ***
authornipkow
Fri Jan 13 14:43:09 2006 +0100 (2006-01-13)
changeset 1867498d380757893
parent 18673 fad60fe1565c
child 18675 333a73034023
*** empty log message ***
NEWS
src/HOL/Set.thy
     1.1 --- a/NEWS	Fri Jan 13 01:13:17 2006 +0100
     1.2 +++ b/NEWS	Fri Jan 13 14:43:09 2006 +0100
     1.3 @@ -216,6 +216,11 @@
     1.4  * Provers/induct: support coinduction as well.  See
     1.5  src/HOL/Library/Coinductive_List.thy for various examples.
     1.6  
     1.7 +* Simplifier: by default the simplifier trace only shows top level rewrites
     1.8 +now. That is, trace_simp_depth_limit is set to 1 by default. Thus there is
     1.9 +less danger of being flooded by the trace. The trace indicates where parts
    1.10 +have been suppressed.
    1.11 +  
    1.12  * Provers/classical: removed obsolete classical version of elim_format
    1.13  attribute; classical elim/dest rules are now treated uniformly when
    1.14  manipulating the claset.
    1.15 @@ -241,6 +246,8 @@
    1.16  25 like -->); output depends on the "iff" print_mode, the default is
    1.17  "A = B" (with priority 50).
    1.18  
    1.19 +* "LEAST x:A. P" expands to "LEAST x. x:A & P" (input only).
    1.20 +
    1.21  * In the context of the assumption "~(s = t)" the Simplifier rewrites
    1.22  "t = s" to False (by simproc "neq_simproc").  For backward
    1.23  compatibility this can be disabled by ML "reset use_neq_simproc".
     2.1 --- a/src/HOL/Set.thy	Fri Jan 13 01:13:17 2006 +0100
     2.2 +++ b/src/HOL/Set.thy	Fri Jan 13 14:43:09 2006 +0100
     2.3 @@ -64,6 +64,8 @@
     2.4  
     2.5    "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3ALL _:_./ _)" [0, 0, 10] 10)
     2.6    "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3EX _:_./ _)" [0, 0, 10] 10)
     2.7 +  "_Bleast"       :: "id => 'a set => bool => 'a"      ("(3LEAST _:_./ _)" [0, 0, 10] 10)
     2.8 +
     2.9  
    2.10  syntax (HOL)
    2.11    "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3! _:_./ _)" [0, 0, 10] 10)
    2.12 @@ -86,6 +88,8 @@
    2.13    "INT x:A. B"  == "INTER A (%x. B)"
    2.14    "ALL x:A. P"  == "Ball A (%x. P)"
    2.15    "EX x:A. P"   == "Bex A (%x. P)"
    2.16 +  "LEAST x:A. P" => "LEAST x. x:A & P"
    2.17 +
    2.18  
    2.19  syntax (output)
    2.20    "_setle"      :: "'a set => 'a set => bool"             ("op <=")
    2.21 @@ -108,6 +112,7 @@
    2.22    Inter         :: "'a set set => 'a set"                 ("\<Inter>_" [90] 90)
    2.23    "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
    2.24    "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
    2.25 +  "_Bleast"     :: "id => 'a set => bool => 'a"           ("(3LEAST_\<in>_./ _)" [0, 0, 10] 10)
    2.26  
    2.27  syntax (HTML output)
    2.28    "_setle"      :: "'a set => 'a set => bool"             ("op \<subseteq>")