1997-06-05 paulson [Thu, 05 Jun 1997 13:29:41 +0200] rev 3407
Removal of radixstring from string_of_int; addition of string_of_indexname
src/Pure/library.ML

1997-06-05 paulson [Thu, 05 Jun 1997 13:28:32 +0200] rev 3406
There was never need for another copy of radixstring...
src/Pure/POLY.ML

1997-06-05 paulson [Thu, 05 Jun 1997 13:27:28 +0200] rev 3405
Numerous simplifications and removal of HOL-isms
Addition of the "simpset" feature (replacing references to \!simpset)
TFL/dcterm.sml TFL/post.sml TFL/rules.new.sml TFL/rules.sig TFL/tfl.sig TFL/tfl.sml TFL/thry.sig TFL/thry.sml TFL/usyntax.sig TFL/usyntax.sml

1997-06-05 paulson [Thu, 05 Jun 1997 13:26:09 +0200] rev 3404
Now loads theory Recdef
src/HOL/ex/ROOT.ML

1997-06-05 paulson [Thu, 05 Jun 1997 13:22:25 +0200] rev 3403
A slight simplification of optstring
The new "simpset" keyword in the "recdef" declaration
src/HOL/thy_syntax.ML

1997-06-05 paulson [Thu, 05 Jun 1997 13:21:41 +0200] rev 3402
Now extracts the predicate variable from induct0 insteead of trying to
predict its name. The new "freeze" function requires this.
src/HOL/indrule.ML

1997-06-05 paulson [Thu, 05 Jun 1997 13:20:18 +0200] rev 3401
Deleted the obsolete "pred_list" relation
src/HOL/List.thy

1997-06-05 paulson [Thu, 05 Jun 1997 13:19:27 +0200] rev 3400
Documented the new distinct_subgoals_tac
doc-src/Ref/tactic.tex

1997-06-05 paulson [Thu, 05 Jun 1997 13:16:12 +0200] rev 3399
A slight simplification of optstring
src/ZF/thy_syntax.ML

1997-06-05 paulson [Thu, 05 Jun 1997 13:15:36 +0200] rev 3398
Now extracts the predicate variable from induct0 insteead of trying to
predict its name
src/ZF/indrule.ML