tuned;
authorwenzelm
Tue, 28 Jul 1998 16:59:15 +0200
changeset 5207 dd4f51adfff3
parent 5206 a3f26b19cd7e
child 5208 cea0adbc7276
tuned;
NEWS
README.html
src/HOL/hologic.ML
--- a/NEWS	Tue Jul 28 16:36:32 1998 +0200
+++ b/NEWS	Tue Jul 28 16:59:15 1998 +0200
@@ -1,3 +1,4 @@
+
 Isabelle NEWS -- history of user-visible changes
 ================================================
 
@@ -6,11 +7,13 @@
 
 *** Overview of INCOMPATIBILITIES (see below for more details) ***
 
-* HOL/inductive requires Inductive.thy as an ancestor;
-* `inj_onto' is now called `inj_on' (which makes more sense)
+* several changes of proof tools (see next section);
+
+* HOL/inductive requires Inductive.thy as an ancestor; `inj_onto' is
+now called `inj_on' (which makes more sense);
 
 * HOL/Relation: renamed the relational operator r^-1 to 'converse'
-  from 'inverse' (for compatibility with ZF and some literature)
+from 'inverse' (for compatibility with ZF and some literature);
 
 
 *** Proof tools ***
@@ -77,7 +80,7 @@
 usual, backup your sources first!);
 
 * new toplevel commands 'thm' and 'thms' for retrieving theorems from
-the current theory context;
+the current theory context, and 'theory' to lookup stored theories;
 
 * new theory section 'nonterminals' for purely syntactic types;
 
@@ -106,10 +109,14 @@
 * HOL/Prod introduces simplification procedure unit_eq_proc rewriting
 (?x::unit) = (); this is made part of the default simpset, which COULD
 MAKE EXISTING PROOFS FAIL under rare circumstances (consider
-'Delsimprocs [unit_eq_proc];' as last resort);
+'Delsimprocs [unit_eq_proc];' as last resort); also note that
+unit_abs_eta_conv is added in order to counter the effect of
+unit_eq_proc on (%u::unit. f u), replacing it by f rather than by
+%u.f();
 
-* HOL/record package: now includes concrete syntax for record terms
-(still lacks important theorems, like surjective pairing and split);
+* HOL/record package: now includes concrete syntax for record types,
+terms, updates; still lacks important theorems, like surjective
+pairing and split;
 
 * HOL/inductive package reorganized and improved: now supports mutual
 definitions such as
@@ -178,6 +185,9 @@
 
 *** Internal programming interfaces ***
 
+* removed global_names compatibility flag -- all theory declarations
+are qualified by default;
+
 * improved the theory data mechanism to support encapsulation (data
 kind name replaced by private Object.kind, acting as authorization
 key); new type-safe user interface via functor TheoryDataFun;
@@ -191,7 +201,8 @@
 * Pure: several new basic modules made available for general use, see
 also src/Pure/README;
 
-* new tactical CHANGED_GOAL for checking that a tactic modifies a subgoal
+* new tactical CHANGED_GOAL for checking that a tactic modifies a
+subgoal;
 
 
 
--- a/README.html	Tue Jul 28 16:36:32 1998 +0200
+++ b/README.html	Tue Jul 28 16:59:15 1998 +0200
@@ -15,7 +15,7 @@
 
 This is the internal repository version of Isabelle.  Starting with
 Isabelle98, the current line of Isabelle introduces many new features,
-but also some imcompatibilities with Isabelle94.  See the
+but also some imcompatibilities with Isabelle94-XX.  See the
 <tt>NEWS</tt> file in the distribution for more details.
 
 
--- a/src/HOL/hologic.ML	Tue Jul 28 16:36:32 1998 +0200
+++ b/src/HOL/hologic.ML	Tue Jul 28 16:59:15 1998 +0200
@@ -31,13 +31,6 @@
   val mk_binop: string -> term * term -> term
   val mk_binrel: string -> term * term -> term
   val dest_bin: string -> typ -> term -> term * term
-  val natT: typ
-  val zero: term
-  val is_zero: term -> bool
-  val mk_Suc: term -> term
-  val dest_Suc: term -> term
-  val mk_nat: int -> term
-  val dest_nat: term -> int
   val unitT: typ
   val unit: term
   val is_unit: term -> bool
@@ -50,6 +43,13 @@
   val prodT_factors: typ -> typ list
   val split_const: typ * typ * typ -> term
   val mk_tuple: typ -> term list -> term
+  val natT: typ
+  val zero: term
+  val is_zero: term -> bool
+  val mk_Suc: term -> term
+  val dest_Suc: term -> term
+  val mk_nat: int -> term
+  val dest_nat: term -> int
 end;
 
 
@@ -125,31 +125,6 @@
   | dest_bin c _ tm = raise TERM ("dest_bin " ^ c, [tm]);
 
 
-(* nat *)
-
-val natT = Type ("nat", []);
-
-
-val zero = Const ("0", natT);
-
-fun is_zero (Const ("0", _)) = true
-  | is_zero _ = false;
-
-
-fun mk_Suc t = Const ("Suc", natT --> natT) $ t;
-
-fun dest_Suc (Const ("Suc", _) $ t) = t
-  | dest_Suc t = raise TERM ("dest_Suc", [t]);
-
-
-fun mk_nat 0 = zero
-  | mk_nat n = mk_Suc (mk_nat (n - 1));
-
-fun dest_nat (Const ("0", _)) = 0
-  | dest_nat (Const ("Suc", _) $ t) = dest_nat t + 1
-  | dest_nat t = raise TERM ("dest_nat", [t]);
-
-
 (* unit *)
 
 val unitT = Type ("unit", []);
@@ -198,4 +173,28 @@
                  mk_tuple T2 (drop (length (prodT_factors T1), tms)))
   | mk_tuple T (t::_) = t;
 
+
+
+(* nat *)
+
+val natT = Type ("nat", []);
+
+val zero = Const ("0", natT);
+
+fun is_zero (Const ("0", _)) = true
+  | is_zero _ = false;
+
+fun mk_Suc t = Const ("Suc", natT --> natT) $ t;
+
+fun dest_Suc (Const ("Suc", _) $ t) = t
+  | dest_Suc t = raise TERM ("dest_Suc", [t]);
+
+fun mk_nat 0 = zero
+  | mk_nat n = mk_Suc (mk_nat (n - 1));
+
+fun dest_nat (Const ("0", _)) = 0
+  | dest_nat (Const ("Suc", _) $ t) = dest_nat t + 1
+  | dest_nat t = raise TERM ("dest_nat", [t]);
+
+
 end;