--- 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;