NEWS
changeset 26874 b2daa27fc0a7
parent 26765 f2ea56490bfb
child 26877 c3bb1f397811
     1.1 --- a/NEWS	Sat May 10 14:13:20 2008 +0200
     1.2 +++ b/NEWS	Mon May 12 22:03:33 2008 +0200
     1.3 @@ -54,15 +54,15 @@
     1.4  
     1.5  In order to increase the readability of the list produced by
     1.6  unused_thms, theorems that have been created by a particular instance
     1.7 -of a theory command such as inductive or fun(ction) are considered to
     1.8 -belong to the same "group", meaning that if at least one theorem in
     1.9 +of a theory command such as 'inductive' or 'function' are considered
    1.10 +to belong to the same "group", meaning that if at least one theorem in
    1.11  this group is used, the other theorems in the same group are no longer
    1.12  reported as unused.  Moreover, if all theorems in the group are
    1.13  unused, only one theorem in the group is displayed.
    1.14  
    1.15  Note that proof objects have to be switched on in order for
    1.16  unused_thms to work properly (i.e. !proofs must be >= 1, which is
    1.17 -usually the case when using ProofGeneral with the default settings).
    1.18 +usually the case when using Proof General with the default settings).
    1.19  
    1.20  * Authentic naming of facts disallows ad-hoc overwriting of previous
    1.21  theorems within the same name space.  INCOMPATIBILITY, need to remove
    1.22 @@ -83,7 +83,7 @@
    1.23  instead.  Added 'ML_val' as mere diagnostic replacement for 'ML'.
    1.24  INCOMPATIBILITY.
    1.25  
    1.26 -* Command 'setup': discontinued implicit version.
    1.27 +* Command 'setup': discontinued implicit version with ML reference.
    1.28  
    1.29  * Instantiation target allows for simultaneous specification of class
    1.30  instance operations together with an instantiation proof.
    1.31 @@ -97,42 +97,42 @@
    1.32  "fact".  INCOMPATIBILITY: need to name facts explicitly in rare
    1.33  situations.
    1.34  
    1.35 -
    1.36 -*** Isar ***
    1.37 -
    1.38 -* Pure: default proof step now includes 'unfold_locales'; hence
    1.39 -'proof' without argument may be used to unfold locale predicates.
    1.40 +* Locale proofs: default proof step now includes 'unfold_locales';
    1.41 +hence 'proof' without argument may be used to unfold locale
    1.42 +predicates.
    1.43  
    1.44  
    1.45  *** Document preparation ***
    1.46  
    1.47 -* Antiquotation "lemma" takes a proposition and a simple method text as argument
    1.48 -and asserts that the proposition is provable by the corresponding method
    1.49 -invocation.  Prints text of proposition, as does antiquotation "prop".  A simple
    1.50 -method text is either a method name or a method name plus (optional) method
    1.51 -arguments in parentheses, mimicing the conventions known from Isar proof text.
    1.52 -Useful for illustration of presented theorems by particular examples.
    1.53 +* Antiquotation "lemma" takes a proposition and a simple method text
    1.54 +as argument and asserts that the proposition is provable by the
    1.55 +corresponding method invocation.  Prints text of proposition, as does
    1.56 +antiquotation "prop".  A simple method text is either a method name or
    1.57 +a method name plus (optional) method arguments in parentheses,
    1.58 +mimicking the conventions known from Isar proof text.  Useful for
    1.59 +illustration of presented theorems by particular examples.
    1.60  
    1.61  
    1.62  *** HOL ***
    1.63  
    1.64 -* Merged theories Wellfounded_Recursion, Accessible_Part and Wellfounded_Relations
    1.65 -  to "Wellfounded.thy"
    1.66 +* Merged theories Wellfounded_Recursion, Accessible_Part and
    1.67 +Wellfounded_Relations to "Wellfounded.thy".
    1.68  
    1.69  * Explicit class "eq" for executable equality.  INCOMPATIBILITY.
    1.70  
    1.71 -* Class finite no longer treats UNIV as class parameter.  Use class enum from
    1.72 -theory Library/Enum instead to achieve a similar effect.  INCOMPATIBILITY.
    1.73 -
    1.74 -* Theory List: rule list_induct2 now has explicitly named cases "Nil" and "Cons".
    1.75 +* Class finite no longer treats UNIV as class parameter.  Use class
    1.76 +enum from theory Library/Enum instead to achieve a similar effect.
    1.77  INCOMPATIBILITY.
    1.78  
    1.79 +* Theory List: rule list_induct2 now has explicitly named cases "Nil"
    1.80 +and "Cons".  INCOMPATIBILITY.
    1.81 +
    1.82  * HOL (and FOL): renamed variables in rules imp_elim and swap.
    1.83  Potential INCOMPATIBILITY.
    1.84  
    1.85 -* Theory Product_Type: duplicated lemmas split_Pair_apply and injective_fst_snd
    1.86 -removed, use split_eta and prod_eqI instead.  Renamed upd_fst to apfst and upd_snd
    1.87 -to apsnd.  INCOMPATIBILITY.
    1.88 +* Theory Product_Type: duplicated lemmas split_Pair_apply and
    1.89 +injective_fst_snd removed, use split_eta and prod_eqI instead.
    1.90 +Renamed upd_fst to apfst and upd_snd to apsnd.  INCOMPATIBILITY.
    1.91  
    1.92  * Theory Nat: removed redundant lemmas that merely duplicate lemmas of
    1.93  the same name in theory Orderings:
    1.94 @@ -170,7 +170,7 @@
    1.95  
    1.96  * Theory Finite_Set: locales ACf, ACe, ACIf, ACIfSL and ACIfSLlin
    1.97  (whose purpose mainly is for various fold_set functionals) have been
    1.98 -abandoned in favour of the existing algebraic classes
    1.99 +abandoned in favor of the existing algebraic classes
   1.100  ab_semigroup_mult, comm_monoid_mult, ab_semigroup_idem_mult,
   1.101  lower_semilattice (resp. upper_semilattice) and linorder.
   1.102  INCOMPATIBILITY.
   1.103 @@ -182,7 +182,7 @@
   1.104  lattices.  The form set-specific version is available as
   1.105  Inductive.lfp_ordinal_induct_set.
   1.106  
   1.107 -* Theorems "power.simps" renamed to "power_int.simps".
   1.108 +* Renamed theorems "power.simps" to "power_int.simps".
   1.109  
   1.110  * Class semiring_div provides basic abstract properties of semirings
   1.111  with division and modulo operations.  Subsumes former class dvd_mod.
   1.112 @@ -208,9 +208,9 @@
   1.113  
   1.114  * Library/ListVector: new theory of arithmetic vector operations.
   1.115  
   1.116 -* Library/Order_Relation: new theory of various orderings as sets of pairs.
   1.117 -  Defines preorders, partial orders, linear orders and well-orders
   1.118 -  on sets and on types.
   1.119 +* Library/Order_Relation: new theory of various orderings as sets of
   1.120 +pairs.  Defines preorders, partial orders, linear orders and
   1.121 +well-orders on sets and on types.
   1.122  
   1.123  * Constants "card", "internal_split", "option_map" now with authentic
   1.124  syntax.  INCOMPATIBILITY.
   1.125 @@ -223,7 +223,7 @@
   1.126  equality.  INCOMPATIBILITY.
   1.127  
   1.128  * Method "induction_scheme" derives user-specified induction rules
   1.129 -from wellfounded induction and completeness of patterns. This factors
   1.130 +from well-founded induction and completeness of patterns. This factors
   1.131  out some operations that are done internally by the function package
   1.132  and makes them available separately. See "HOL/ex/Induction_Scheme.thy"
   1.133  for examples,
   1.134 @@ -235,31 +235,32 @@
   1.135  * Metis prover is now an order of magnitude faster, and also works
   1.136  with multithreading.
   1.137  
   1.138 -* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
   1.139 -
   1.140 -* Sledgehammer no longer produces structured proofs by default. To enable, 
   1.141 -declare [[sledgehammer_full = true]]. Attributes reconstruction_modulus,  
   1.142 -reconstruction_sorts renamed sledgehammer_modulus, sledgehammer_sorts. 
   1.143 -INCOMPATIBILITY.
   1.144 +* Metis: the maximum number of clauses that can be produced from a
   1.145 +theorem is now given by the attribute max_clauses. Theorems that
   1.146 +exceed this number are ignored, with a warning printed.
   1.147 +
   1.148 +* Sledgehammer no longer produces structured proofs by default. To
   1.149 +enable, declare [[sledgehammer_full = true]]. Attributes
   1.150 +reconstruction_modulus, reconstruction_sorts renamed
   1.151 +sledgehammer_modulus, sledgehammer_sorts.  INCOMPATIBILITY.
   1.152 +
   1.153  
   1.154  *** ZF ***
   1.155  
   1.156 -* Renamed theories:
   1.157 -
   1.158 -  Datatype.thy  -> Datatype_ZF.thy
   1.159 -  Inductive.thy -> Inductive_ZF.thy
   1.160 -  Int.thy       -> Int_ZF.thy
   1.161 -  IntDiv.thy    -> IntDiv_ZF.thy
   1.162 -  Nat.thy       -> Nat_ZF.thy
   1.163 -  List.thy      -> List_ZF.thy
   1.164 -  Main.thy      -> Main_ZF.thy
   1.165 -
   1.166 - This is to allow to load both ZF and HOL in the same session.
   1.167 -
   1.168 - INCOMPATIBILITY: ZF theories that import individual theories below
   1.169 - Main might need to be adapted. For compatibility, a new 
   1.170 - "theory Main imports Main_ZF begin end" is provided, so if you just
   1.171 - imported "Main", no changes are needed.
   1.172 +* Renamed some theories to allow to loading both ZF and HOL in the
   1.173 +same session:
   1.174 +
   1.175 +  Datatype  -> Datatype_ZF
   1.176 +  Inductive -> Inductive_ZF
   1.177 +  Int       -> Int_ZF
   1.178 +  IntDiv    -> IntDiv_ZF
   1.179 +  Nat       -> Nat_ZF
   1.180 +  List      -> List_ZF
   1.181 +  Main      -> Main_ZF
   1.182 +
   1.183 +INCOMPATIBILITY: ZF theories that import individual theories below
   1.184 +Main might need to be adapted.  Regular theory Main is still
   1.185 +available, as trivial extension of Main_ZF.
   1.186  
   1.187  
   1.188  *** ML ***
   1.189 @@ -278,9 +279,9 @@
   1.190  management only; user-code should use print_mode_value,
   1.191  print_mode_active, PrintMode.setmp etc.  INCOMPATIBILITY.
   1.192  
   1.193 -* system/system_out provides a robust way to invoke external shell
   1.194 -commands, with propagation of interrupts (after Poly/ML 5.2).  Do not
   1.195 -use OS.Process.system etc. directly.
   1.196 +* Functions system/system_out provide a robust way to invoke external
   1.197 +shell commands, with propagation of interrupts (after Poly/ML 5.2).
   1.198 +Do not use OS.Process.system etc. from the basis library!
   1.199  
   1.200  
   1.201  *** System ***