summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Tue, 28 Jul 1998 16:59:15 +0200 | |

changeset 5207 | dd4f51adfff3 |

parent 5206 | a3f26b19cd7e |

child 5208 | cea0adbc7276 |

tuned;

NEWS | file | annotate | diff | comparison | revisions | |

README.html | file | annotate | diff | comparison | revisions | |

src/HOL/hologic.ML | file | annotate | diff | comparison | revisions |

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