1998-01-08 paulson [Thu, 08 Jan 1998 18:10:34 +0100] rev 4537
Expressed most Oops rules using Notes instead of Says, and other tidying
src/HOL/Auth/NS_Shared.ML src/HOL/Auth/NS_Shared.thy src/HOL/Auth/OtwayRees.ML src/HOL/Auth/OtwayRees.thy src/HOL/Auth/OtwayRees_AN.ML src/HOL/Auth/OtwayRees_AN.thy src/HOL/Auth/OtwayRees_Bad.ML src/HOL/Auth/OtwayRees_Bad.thy src/HOL/Auth/Yahalom.ML src/HOL/Auth/Yahalom.thy src/HOL/Auth/Yahalom2.ML src/HOL/Auth/Yahalom2.thy

1998-01-08 oheimb [Thu, 08 Jan 1998 18:09:47 +0100] rev 4536
added split_paired_Ex to the implicit simpset
src/HOL/thy_syntax.ML src/HOLCF/IOA/meta_theory/Automata.ML src/HOLCF/IOA/meta_theory/Traces.ML

1998-01-08 oheimb [Thu, 08 Jan 1998 18:09:07 +0100] rev 4535
added select_equality to the implicit claset
src/HOL/Induct/LFilter.ML src/HOL/NatDef.ML src/HOL/Sexp.ML src/HOL/Sum.ML src/HOL/Univ.ML src/HOL/cladata.ML src/HOLCF/Sprod0.ML src/HOLCF/Ssum0.ML src/HOLCF/Ssum1.ML

1998-01-08 oheimb [Thu, 08 Jan 1998 18:08:43 +0100] rev 4534
added select_equality to the implicit claset
added split_paired_Ex, split_part, and Eps_split_eq to the implicit simpset
removed split_select
renamed Collect_Prod to Collect_split
src/HOL/Prod.ML

1998-01-08 oheimb [Thu, 08 Jan 1998 18:07:06 +0100] rev 4533
added newline at end of file
src/HOLCF/IOA/meta_theory/IOA.ML

1998-01-08 oheimb [Thu, 08 Jan 1998 18:06:21 +0100] rev 4532
*** empty log message ***
src/HOLCF/IOA/NTP/Lemmas.ML

1998-01-08 oheimb [Thu, 08 Jan 1998 18:03:36 +0100] rev 4531
streamlined specification of included theories
src/HOL/Quot/NPAIR.thy src/HOL/Quot/PER.thy

1998-01-08 oheimb [Thu, 08 Jan 1998 18:00:42 +0100] rev 4530
corrected Title
src/HOL/IOA/Asig.ML src/HOL/IOA/Asig.thy src/HOL/IOA/IOA.ML src/HOL/IOA/IOA.thy src/HOL/IOA/Solve.ML src/HOL/IOA/Solve.thy

1998-01-08 oheimb [Thu, 08 Jan 1998 18:00:08 +0100] rev 4529
removed obsolete comment
src/HOL/IOA/ROOT.ML

1998-01-08 oheimb [Thu, 08 Jan 1998 17:56:32 +0100] rev 4528
added Univalent
src/HOL/Relation.thy