1998-11-27 paulson [Fri, 27 Nov 1998 16:46:01 +0100] rev 5981
fixed a link
src/HOL/Real/Hyperreal/README.html

1998-11-27 paulson [Fri, 27 Nov 1998 13:13:22 +0100] rev 5980
added Real/Hyperreal
src/HOL/IsaMakefile

1998-11-27 paulson [Fri, 27 Nov 1998 11:24:27 +0100] rev 5979
Addition of Hyperreal theories Zorn and Filter
src/HOL/Real/Hyperreal/Filter.ML src/HOL/Real/Hyperreal/Filter.thy src/HOL/Real/Hyperreal/README.html src/HOL/Real/Hyperreal/ROOT.ML src/HOL/Real/Hyperreal/Zorn.ML src/HOL/Real/Hyperreal/Zorn.thy src/HOL/Real/ROOT.ML

1998-11-27 paulson [Fri, 27 Nov 1998 10:40:29 +0100] rev 5978
moved diag (diagonal relation) from Univ to Relation
src/HOL/Relation.ML src/HOL/Relation.thy src/HOL/Univ.ML src/HOL/Univ.thy

1998-11-26 paulson [Thu, 26 Nov 1998 17:40:10 +0100] rev 5977
tidied up list definitions, using type 'a option instead of
unit + 'a, also using real typedefs instead of faking them with extra rules
src/HOL/Induct/LFilter.thy src/HOL/Induct/LList.ML src/HOL/Induct/LList.thy src/HOL/Induct/SList.ML src/HOL/Induct/SList.thy

1998-11-26 mueller [Thu, 26 Nov 1998 16:37:56 +0100] rev 5976
tuning to assimiliate it with PhD;
src/HOLCF/IOA/meta_theory/Abstraction.ML src/HOLCF/IOA/meta_theory/Abstraction.thy src/HOLCF/IOA/meta_theory/Automata.ML src/HOLCF/IOA/meta_theory/CompoScheds.ML src/HOLCF/IOA/meta_theory/Compositionality.ML src/HOLCF/IOA/meta_theory/LiveIOA.ML src/HOLCF/IOA/meta_theory/Pred.thy src/HOLCF/IOA/meta_theory/RefCorrectness.thy src/HOLCF/IOA/meta_theory/Seq.ML src/HOLCF/IOA/meta_theory/Seq.thy src/HOLCF/IOA/meta_theory/Sequence.ML src/HOLCF/IOA/meta_theory/ShortExecutions.ML src/HOLCF/IOA/meta_theory/TL.ML src/HOLCF/IOA/meta_theory/TL.thy src/HOLCF/IOA/meta_theory/TLS.ML src/HOLCF/IOA/meta_theory/TLS.thy src/HOLCF/IOA/meta_theory/Traces.thy

1998-11-26 nipkow [Thu, 26 Nov 1998 12:18:51 +0100] rev 5975
Added a general refutation tactic which works by putting things into nnf first.
src/HOL/simpdata.ML

1998-11-26 nipkow [Thu, 26 Nov 1998 12:18:08 +0100] rev 5974
Added filter_prems_tac
src/Pure/tactic.ML

1998-11-25 wenzelm [Wed, 25 Nov 1998 20:55:25 +0100] rev 5973
removed prs / prs_fn;
NEWS

1998-11-25 paulson [Wed, 25 Nov 1998 15:55:00 +0100] rev 5972
guarantees laws
src/HOL/UNITY/PPROD.ML src/HOL/UNITY/PPROD.thy