summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

NEWS

changeset 5125 | 463a0e9df5b5 |

parent 5109 | b3d18eb3ac20 |

child 5127 | ef467e05da61 |

1.1 --- a/NEWS Fri Jul 03 17:35:39 1998 +0200 1.2 +++ b/NEWS Fri Jul 03 17:36:45 1998 +0200 1.3 @@ -46,6 +46,14 @@ 1.4 1.5 *** HOL *** 1.6 1.7 +* reorganized the main HOL image: HOL/Integ and String loaded by 1.8 +default; theory Main includes everything; 1.9 + 1.10 +* HOL/Real: a construction of the reals using Dedekind cuts; 1.11 + 1.12 +* HOL/record: now includes concrete syntax for record terms (still 1.13 +lacks important theorems, like surjective pairing and split); 1.14 + 1.15 * Inductive definition package: Mutually recursive definitions such as 1.16 1.17 inductive EVEN ODD 1.18 @@ -60,11 +68,6 @@ 1.19 the recursive sets. Note that the component "mutual_induct" no longer 1.20 exists - the induction rule is always contained in "induct". 1.21 1.22 -* HOL/Real: a construction of the reals using Dedekind cuts 1.23 - 1.24 -* HOL/record: now includes concrete syntax for record terms (still 1.25 -lacks important theorems, like surjective pairing and split); 1.26 - 1.27 * simplification procedure unit_eq_proc rewrites (?x::unit) = (); this 1.28 is made part of the default simpset of Prod.thy, which COULD MAKE 1.29 EXISTING PROOFS FAIL (consider 'Delsimprocs [unit_eq_proc];' as last 1.30 @@ -74,9 +77,9 @@ 1.31 rewriting and classical reasoning (and whatever other tools) similarly 1.32 to auto_tac, but is aimed to solve the given subgoal totally; 1.33 1.34 -* added option_map_eq_Some to simpset() and claset() 1.35 +* added option_map_eq_Some to simpset() and claset(); 1.36 1.37 -* New directory HOL/UNITY: Chandy and Misra's UNITY formalism 1.38 +* New directory HOL/UNITY: Chandy and Misra's UNITY formalism; 1.39 1.40 * New theory HOL/Update of function updates: 1.41 f(a:=b) == %x. if x=a then b else f x