# HG changeset patch # User wenzelm # Date 1193249868 -7200 # Node ID f9ced25685e0181e0877d2d9dd235852dad6c8c1 # Parent c5f80d70537e81d554572022271e464cd0f223e8 tuned file names etc.; diff -r c5f80d70537e -r f9ced25685e0 NEWS --- a/NEWS Wed Oct 24 19:46:01 2007 +0200 +++ b/NEWS Wed Oct 24 20:17:48 2007 +0200 @@ -117,7 +117,7 @@ context). Within the body context of a 'class' target, a separate syntax layer ("user space type system") takes care of converting between global polymorphic consts and internal locale representation. -See HOL/ex/Classpackage.thy for examples (as well as main HOL). +See src/HOL/ex/Classpackage.thy for examples (as well as main HOL). * Yet another code generator framework allows to generate executable code for ML and Haskell (including Isabelle classes). A short usage @@ -159,8 +159,8 @@ code_instance and code_class only apply to target Haskell. -For example usage see HOL/ex/Codegenerator.thy and -HOL/ex/Codegenerator_Pretty.thy. A separate tutorial on code +For example usage see src/HOL/ex/Codegenerator.thy and +src/HOL/ex/Codegenerator_Pretty.thy. A separate tutorial on code generation from Isabelle/HOL theories is available via "isatool doc codegen". @@ -412,7 +412,7 @@ constant name is qualified by the locale base name. An internal abbreviation takes care for convenient input and output, making the parameters implicit and using the original short name. See also -HOL/ex/Abstract_NAT.thy for an example of deriving polymorphic +src/HOL/ex/Abstract_NAT.thy for an example of deriving polymorphic entities from a monomorphic theory. Presently, abbreviations are only available 'in' a target locale, but @@ -480,14 +480,15 @@ connectives !! and ==> are rarely required anymore in inductive goals (using object-logic connectives for this purpose has been long obsolete anyway). Common proof patterns are explained in -HOL/Induct/Common_Patterns.thy, see also HOL/Isar_examples/Puzzle.thy -and src/HOL/Lambda for realistic examples. +src/HOL/Induct/Common_Patterns.thy, see also +src/HOL/Isar_examples/Puzzle.thy and src/HOL/Lambda for realistic +examples. * Method "induct": improved handling of simultaneous goals. Instead of introducing object-level conjunction, the statement is now split into several conclusions, while the corresponding symbolic cases are nested accordingly. INCOMPATIBILITY, proofs need to be structured explicitly, -see HOL/Induct/Common_Patterns.thy, for example. +see src/HOL/Induct/Common_Patterns.thy, for example. * Method "induct": mutual induction rules are now specified as a list of rule sharing the same induction cases. HOL packages usually provide @@ -676,8 +677,8 @@ if the additional syntax "p ..." is required. - Numerous examples can be found in the subdirectories HOL/Auth, HOL/Bali, - HOL/Induct, and HOL/MicroJava. + Numerous examples can be found in the subdirectories src/HOL/Auth, + src/HOL/Bali, src/HOL/Induct, and src/HOL/MicroJava. INCOMPATIBILITIES: @@ -789,7 +790,7 @@ Special syntax: "SUM x <- xs. f x" (and latex variants) * New syntax for Haskell-like list comprehension (input only), eg. -[(x,y). x <- xs, y <- ys, x ~= y], see also HOL/List.thy. +[(x,y). x <- xs, y <- ys, x ~= y], see also src/HOL/List.thy. * The special syntax for function "filter" has changed from [x : xs. P] to [x <- xs. P] to avoid an ambiguity caused by list @@ -801,7 +802,7 @@ * Renamed lemma "set_take_whileD" to "set_takeWhileD". -* New functions "sorted" and "sort" in HOL/List.thy. +* New functions "sorted" and "sort" in src/HOL/List.thy. * Function "sgn" is now overloaded and available on int, real, complex (and other numeric types), using class "sgn". Two possible defs of @@ -819,7 +820,7 @@ ring_distribs. Removed lemmas field_xyz in theory Ring_and_Field because they were subsumed by lemmas xyz. INCOMPATIBILITY. -* Library/Commutative_Ring.thy: switched from recdef to function +* Theory Library/Commutative_Ring: switched from recdef to function package; constants add, mul, pow now curried. Infix syntax for algebraic operations. @@ -1003,14 +1004,14 @@ - Numeral simplification theorems named Numeral.numeral_simps instead of Bin_simps. - ML structure Bin_Simprocs now named Int_Numeral_Base_Simprocs. -See HOL/Integ/IntArith.thy for an example setup. - -* Command 'normal_form' computes the normal form of a -term that may contain free variables. For example -``normal_form "rev [a, b, c]"'' produces ``[b, c, a]'' (without proof). -This command is suitable for heavy-duty computations because the functions -are compiled to ML first. Correspondingly, a method ``normalization'' -is provided. See further HOL/ex/NormalForm.thy and Tools/nbe.ML. +See src/HOL/Integ/IntArith.thy for an example setup. + +* Command 'normal_form' computes the normal form of a term that may +contain free variables. For example ``normal_form "rev [a, b, c]"'' +produces ``[b, c, a]'' (without proof). This command is suitable for +heavy-duty computations because the functions are compiled to ML +first. Correspondingly, a method "normalization" is provided. See +further src/HOL/ex/NormalForm.thy and src/Tools/nbe.ML. * Alternative iff syntax "A <-> B" for equality on bool (with priority 25 like -->); output depends on the "iff" print_mode, the default is @@ -1120,10 +1121,10 @@ generattion). The method uses reify to compute s and xs as above then applies corr_thm and uses normalization by evaluation to "prove" f s = r and finally gets the theorem t = r, which is again applied to the -subgoal. An Example is available in HOL/ex/ReflectionEx.thy. - -* Reflection: Automatic reification now handels binding, an example -is available in HOL/ex/ReflectionEx.thy +subgoal. An Example is available in src/HOL/ex/ReflectionEx.thy. + +* Reflection: Automatic reification now handels binding, an example is +available in src/HOL/ex/ReflectionEx.thy *** HOL-Complex *** @@ -1202,8 +1203,8 @@ *** HOL-Nominal *** * Substantial, yet incomplete support for nominal datatypes (binding -structures) based on HOL-Nominal logic. See HOL/Nominal and -HOL/Nominal/Examples. Prespective users should consult +structures) based on HOL-Nominal logic. See src/HOL/Nominal and +src/HOL/Nominal/Examples. Prospective users should consult http://isabelle.in.tum.de/nominal/