simplification procedure unit_eq_proc rewrites (?x::unit) = ();
authorwenzelm
Thu Jun 25 16:12:02 1998 +0200 (1998-06-25)
changeset 50858e5a7942fdea
parent 5084 a676ada3b380
child 5086 ef479934678b
simplification procedure unit_eq_proc rewrites (?x::unit) = ();
quote / antiquote translations;
NEWS
     1.1 --- a/NEWS	Thu Jun 25 15:37:36 1998 +0200
     1.2 +++ b/NEWS	Thu Jun 25 16:12:02 1998 +0200
     1.3 @@ -49,6 +49,11 @@
     1.4  * HOL/record: now includes concrete syntax for record terms (still
     1.5  lacks important theorems, like surjective pairing and split);
     1.6  
     1.7 +* simplification procedure unit_eq_proc rewrites (?x::unit) = (); this
     1.8 +is made part of the default simpset of Prod.thy, which COULD MAKE
     1.9 +EXISTING PROOFS FAIL (consider 'Delsimprocs [unit_eq_proc];' as last
    1.10 +resort);
    1.11 +
    1.12  * new force_tac (and its derivations Force_tac, force): combines
    1.13  rewriting and classical reasoning (and whatever other tools) similarly
    1.14  to auto_tac, but is aimed to solve the given subgoal totally;
    1.15 @@ -124,6 +129,9 @@
    1.16  kind name replaced by private Object.kind, acting as authorization
    1.17  key); new type-safe user interface via functor TheoryDataFun;
    1.18  
    1.19 +* module Pure/Syntax now offers quote / antiquote translation
    1.20 +functions (useful for Hoare logic etc. with implicit dependencies);
    1.21 +
    1.22  
    1.23  
    1.24  New in Isabelle98 (January 1998)