1997-05-26 paulson [Mon, 26 May 1997 12:32:35 +0200] rev 3334
Simplified proofs using expand_option_case
src/HOL/Subst/Unify.ML

1997-05-26 paulson [Mon, 26 May 1997 12:29:55 +0200] rev 3333
Now checks the name of the function being defined;
More de-HOL-ification
TFL/tfl.sig TFL/tfl.sml

1997-05-26 paulson [Mon, 26 May 1997 12:29:10 +0200] rev 3332
More de-HOL-ification
TFL/rules.new.sml TFL/thry.sml

1997-05-26 paulson [Mon, 26 May 1997 12:28:30 +0200] rev 3331
Now checks the name of the function being defined
TFL/post.sml

1997-05-26 paulson [Mon, 26 May 1997 12:27:58 +0200] rev 3330
Deleted unused functions
TFL/dcterm.sml TFL/usyntax.sig TFL/usyntax.sml TFL/utils.sig TFL/utils.sml

1997-05-26 paulson [Mon, 26 May 1997 12:26:35 +0200] rev 3329
Now a Perl script. No longer requires commands to be at the beginnings of
lines. RESTRICTION: no longer expands tabs to spaces. No longer lists the
files it is altering.
src/Tools/expandshort

1997-05-26 paulson [Mon, 26 May 1997 12:25:15 +0200] rev 3328
Slight simplifications
src/ZF/ex/Primrec.ML

1997-05-25 slotosch [Sun, 25 May 1997 18:45:25 +0200] rev 3327
Eliminated ccc1. Moved ID,oo into Cfun.
src/HOLCF/Cfun3.ML src/HOLCF/Cfun3.thy src/HOLCF/Fun1.thy src/HOLCF/HOLCF.thy src/HOLCF/Lift1.thy src/HOLCF/Tr.thy src/HOLCF/Up3.ML src/HOLCF/ccc1.ML src/HOLCF/ccc1.thy

1997-05-25 slotosch [Sun, 25 May 1997 16:59:40 +0200] rev 3326
Moved the classes flat chfin from Fix to Pcpo.
Corresponding theorems from Fix into Pcpo,Cont,Cfun3
src/HOLCF/Cfun3.ML src/HOLCF/Cont.ML src/HOLCF/Fix.ML src/HOLCF/Fix.thy src/HOLCF/Pcpo.ML src/HOLCF/Pcpo.thy

1997-05-25 slotosch [Sun, 25 May 1997 16:57:19 +0200] rev 3325
*** empty log message ***
src/HOLCF/IMP/Denotational.ML