tuned;
authorwenzelm
Tue Jul 28 16:59:15 1998 +0200 (1998-07-28)
changeset 5207dd4f51adfff3
parent 5206 a3f26b19cd7e
child 5208 cea0adbc7276
tuned;
NEWS
README.html
src/HOL/hologic.ML
     1.1 --- a/NEWS	Tue Jul 28 16:36:32 1998 +0200
     1.2 +++ b/NEWS	Tue Jul 28 16:59:15 1998 +0200
     1.3 @@ -1,3 +1,4 @@
     1.4 +
     1.5  Isabelle NEWS -- history of user-visible changes
     1.6  ================================================
     1.7  
     1.8 @@ -6,11 +7,13 @@
     1.9  
    1.10  *** Overview of INCOMPATIBILITIES (see below for more details) ***
    1.11  
    1.12 -* HOL/inductive requires Inductive.thy as an ancestor;
    1.13 -* `inj_onto' is now called `inj_on' (which makes more sense)
    1.14 +* several changes of proof tools (see next section);
    1.15 +
    1.16 +* HOL/inductive requires Inductive.thy as an ancestor; `inj_onto' is
    1.17 +now called `inj_on' (which makes more sense);
    1.18  
    1.19  * HOL/Relation: renamed the relational operator r^-1 to 'converse'
    1.20 -  from 'inverse' (for compatibility with ZF and some literature)
    1.21 +from 'inverse' (for compatibility with ZF and some literature);
    1.22  
    1.23  
    1.24  *** Proof tools ***
    1.25 @@ -77,7 +80,7 @@
    1.26  usual, backup your sources first!);
    1.27  
    1.28  * new toplevel commands 'thm' and 'thms' for retrieving theorems from
    1.29 -the current theory context;
    1.30 +the current theory context, and 'theory' to lookup stored theories;
    1.31  
    1.32  * new theory section 'nonterminals' for purely syntactic types;
    1.33  
    1.34 @@ -106,10 +109,14 @@
    1.35  * HOL/Prod introduces simplification procedure unit_eq_proc rewriting
    1.36  (?x::unit) = (); this is made part of the default simpset, which COULD
    1.37  MAKE EXISTING PROOFS FAIL under rare circumstances (consider
    1.38 -'Delsimprocs [unit_eq_proc];' as last resort);
    1.39 +'Delsimprocs [unit_eq_proc];' as last resort); also note that
    1.40 +unit_abs_eta_conv is added in order to counter the effect of
    1.41 +unit_eq_proc on (%u::unit. f u), replacing it by f rather than by
    1.42 +%u.f();
    1.43  
    1.44 -* HOL/record package: now includes concrete syntax for record terms
    1.45 -(still lacks important theorems, like surjective pairing and split);
    1.46 +* HOL/record package: now includes concrete syntax for record types,
    1.47 +terms, updates; still lacks important theorems, like surjective
    1.48 +pairing and split;
    1.49  
    1.50  * HOL/inductive package reorganized and improved: now supports mutual
    1.51  definitions such as
    1.52 @@ -178,6 +185,9 @@
    1.53  
    1.54  *** Internal programming interfaces ***
    1.55  
    1.56 +* removed global_names compatibility flag -- all theory declarations
    1.57 +are qualified by default;
    1.58 +
    1.59  * improved the theory data mechanism to support encapsulation (data
    1.60  kind name replaced by private Object.kind, acting as authorization
    1.61  key); new type-safe user interface via functor TheoryDataFun;
    1.62 @@ -191,7 +201,8 @@
    1.63  * Pure: several new basic modules made available for general use, see
    1.64  also src/Pure/README;
    1.65  
    1.66 -* new tactical CHANGED_GOAL for checking that a tactic modifies a subgoal
    1.67 +* new tactical CHANGED_GOAL for checking that a tactic modifies a
    1.68 +subgoal;
    1.69  
    1.70  
    1.71  
     2.1 --- a/README.html	Tue Jul 28 16:36:32 1998 +0200
     2.2 +++ b/README.html	Tue Jul 28 16:59:15 1998 +0200
     2.3 @@ -15,7 +15,7 @@
     2.4  
     2.5  This is the internal repository version of Isabelle.  Starting with
     2.6  Isabelle98, the current line of Isabelle introduces many new features,
     2.7 -but also some imcompatibilities with Isabelle94.  See the
     2.8 +but also some imcompatibilities with Isabelle94-XX.  See the
     2.9  <tt>NEWS</tt> file in the distribution for more details.
    2.10  
    2.11  
     3.1 --- a/src/HOL/hologic.ML	Tue Jul 28 16:36:32 1998 +0200
     3.2 +++ b/src/HOL/hologic.ML	Tue Jul 28 16:59:15 1998 +0200
     3.3 @@ -31,13 +31,6 @@
     3.4    val mk_binop: string -> term * term -> term
     3.5    val mk_binrel: string -> term * term -> term
     3.6    val dest_bin: string -> typ -> term -> term * term
     3.7 -  val natT: typ
     3.8 -  val zero: term
     3.9 -  val is_zero: term -> bool
    3.10 -  val mk_Suc: term -> term
    3.11 -  val dest_Suc: term -> term
    3.12 -  val mk_nat: int -> term
    3.13 -  val dest_nat: term -> int
    3.14    val unitT: typ
    3.15    val unit: term
    3.16    val is_unit: term -> bool
    3.17 @@ -50,6 +43,13 @@
    3.18    val prodT_factors: typ -> typ list
    3.19    val split_const: typ * typ * typ -> term
    3.20    val mk_tuple: typ -> term list -> term
    3.21 +  val natT: typ
    3.22 +  val zero: term
    3.23 +  val is_zero: term -> bool
    3.24 +  val mk_Suc: term -> term
    3.25 +  val dest_Suc: term -> term
    3.26 +  val mk_nat: int -> term
    3.27 +  val dest_nat: term -> int
    3.28  end;
    3.29  
    3.30  
    3.31 @@ -125,31 +125,6 @@
    3.32    | dest_bin c _ tm = raise TERM ("dest_bin " ^ c, [tm]);
    3.33  
    3.34  
    3.35 -(* nat *)
    3.36 -
    3.37 -val natT = Type ("nat", []);
    3.38 -
    3.39 -
    3.40 -val zero = Const ("0", natT);
    3.41 -
    3.42 -fun is_zero (Const ("0", _)) = true
    3.43 -  | is_zero _ = false;
    3.44 -
    3.45 -
    3.46 -fun mk_Suc t = Const ("Suc", natT --> natT) $ t;
    3.47 -
    3.48 -fun dest_Suc (Const ("Suc", _) $ t) = t
    3.49 -  | dest_Suc t = raise TERM ("dest_Suc", [t]);
    3.50 -
    3.51 -
    3.52 -fun mk_nat 0 = zero
    3.53 -  | mk_nat n = mk_Suc (mk_nat (n - 1));
    3.54 -
    3.55 -fun dest_nat (Const ("0", _)) = 0
    3.56 -  | dest_nat (Const ("Suc", _) $ t) = dest_nat t + 1
    3.57 -  | dest_nat t = raise TERM ("dest_nat", [t]);
    3.58 -
    3.59 -
    3.60  (* unit *)
    3.61  
    3.62  val unitT = Type ("unit", []);
    3.63 @@ -198,4 +173,28 @@
    3.64                   mk_tuple T2 (drop (length (prodT_factors T1), tms)))
    3.65    | mk_tuple T (t::_) = t;
    3.66  
    3.67 +
    3.68 +
    3.69 +(* nat *)
    3.70 +
    3.71 +val natT = Type ("nat", []);
    3.72 +
    3.73 +val zero = Const ("0", natT);
    3.74 +
    3.75 +fun is_zero (Const ("0", _)) = true
    3.76 +  | is_zero _ = false;
    3.77 +
    3.78 +fun mk_Suc t = Const ("Suc", natT --> natT) $ t;
    3.79 +
    3.80 +fun dest_Suc (Const ("Suc", _) $ t) = t
    3.81 +  | dest_Suc t = raise TERM ("dest_Suc", [t]);
    3.82 +
    3.83 +fun mk_nat 0 = zero
    3.84 +  | mk_nat n = mk_Suc (mk_nat (n - 1));
    3.85 +
    3.86 +fun dest_nat (Const ("0", _)) = 0
    3.87 +  | dest_nat (Const ("Suc", _) $ t) = dest_nat t + 1
    3.88 +  | dest_nat t = raise TERM ("dest_nat", [t]);
    3.89 +
    3.90 +
    3.91  end;