2001-10-04 wenzelm [Thu, 04 Oct 2001 11:22:10 +0200] rev 11661
updated;
etc/isar-keywords.el

2001-10-04 berghofe [Thu, 04 Oct 2001 00:53:27 +0200] rev 11660
Fixed bug in decompose.
src/Pure/Proof/reconstruct.ML

2001-10-03 wenzelm [Wed, 03 Oct 2001 21:03:05 +0200] rev 11659
Tools/induct_attrib.ML now part of Pure;
src/HOL/IsaMakefile src/HOL/Typedef.thy

2001-10-03 wenzelm [Wed, 03 Oct 2001 21:01:53 +0200] rev 11658
Isar/induct_attrib.ML;
src/Pure/IsaMakefile src/Pure/Isar/ROOT.ML src/Pure/Isar/induct_attrib.ML src/Pure/pure.ML

2001-10-03 wenzelm [Wed, 03 Oct 2001 20:58:27 +0200] rev 11657
*** empty log message ***
NEWS

2001-10-03 wenzelm [Wed, 03 Oct 2001 20:55:31 +0200] rev 11656
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
src/HOL/Tools/induct_attrib.ML src/Pure/Isar/induct_attrib.ML

2001-10-03 wenzelm [Wed, 03 Oct 2001 20:54:16 +0200] rev 11655
tuned parentheses in relational expressions;
src/HOL/Auth/KerberosIV.ML src/HOL/Auth/Kerberos_BAN.ML src/HOL/Auth/NS_Shared.thy src/HOL/Auth/OtwayRees.thy src/HOL/Auth/OtwayRees_AN.thy src/HOL/Auth/OtwayRees_Bad.thy src/HOL/Auth/Recur.thy src/HOL/Auth/TLS.thy src/HOL/Auth/Yahalom.thy src/HOL/Auth/Yahalom2.thy src/HOL/Auth/Yahalom_Bad.thy src/HOL/Hyperreal/HyperDef.ML src/HOL/Hyperreal/HyperNat.ML src/HOL/Hyperreal/NSA.ML src/HOL/Integ/Bin.ML src/HOL/Integ/IntDef.ML src/HOL/Library/Multiset.thy src/HOL/Library/Nat_Infinity.thy src/HOL/NatArith.thy src/HOL/NatDef.ML src/HOL/Option.ML src/HOL/Real/HahnBanach/Subspace.thy src/HOL/Real/PNat.ML src/HOL/Real/PRat.ML src/HOL/Real/PReal.ML src/HOL/Real/RealDef.ML src/HOL/Relation.ML src/HOL/Set.ML src/HOL/equalities.ML src/HOLCF/FOCUS/Buffer.ML src/HOLCF/FOCUS/Buffer_adm.ML src/HOLCF/FOCUS/Fstream.ML src/HOLCF/FOCUS/Stream_adm.thy src/HOLCF/IOA/meta_theory/Automata.ML src/HOLCF/IOA/meta_theory/CompoExecs.ML src/HOLCF/IOA/meta_theory/CompoScheds.ML src/HOLCF/IOA/meta_theory/CompoTraces.ML src/HOLCF/Lift3.ML src/HOLCF/Tr.ML src/HOLCF/ex/Stream.ML

2001-10-03 wenzelm [Wed, 03 Oct 2001 20:54:05 +0200] rev 11654
moved linorder_cases to theory Ord;
src/HOL/Typedef.thy

2001-10-03 wenzelm [Wed, 03 Oct 2001 20:53:02 +0200] rev 11653
linorder_cases supersedes linorder_less_split;
tuned parentheses in relational expressions;
src/HOL/Ord.thy

2001-10-03 paulson [Wed, 03 Oct 2001 11:45:24 +0200] rev 11652
eta-expansion required for SML/NJ
src/Pure/proofterm.ML