1998-08-06 paulson [Thu, 06 Aug 1998 15:48:13 +0200] rev 5278
even more tidying of Goal commands
src/HOL/Auth/NS_Shared.ML src/HOL/Auth/OtwayRees.ML src/HOL/Auth/OtwayRees_AN.ML src/HOL/Auth/OtwayRees_Bad.ML src/HOL/Auth/Shared.ML src/HOL/Divides.ML src/HOL/Finite.ML src/HOL/IMP/Hoare.ML src/HOL/IMP/Transition.ML src/HOL/IMP/VC.ML src/HOL/Induct/LList.ML src/HOL/Induct/SList.ML src/HOL/Induct/Term.ML src/HOL/Integ/Equiv.ML src/HOL/Integ/Integ.ML src/HOL/List.ML src/HOL/Prod.ML src/HOL/RelPow.ML src/HOL/Sexp.ML src/HOL/Subst/Subst.ML src/HOL/Subst/Unifier.ML src/HOL/Subst/Unify.ML src/HOL/Univ.ML src/HOL/WF.ML src/HOL/equalities.ML src/HOL/ex/MT.ML src/HOL/ex/Qsort.ML src/HOL/ex/StringEx.ML src/HOL/ex/cla.ML src/HOL/simpdata.ML

1998-08-06 paulson [Thu, 06 Aug 1998 15:47:26 +0200] rev 5277
A higher-level treatment of LeadsTo, minimizing use of "reachable"
src/HOL/UNITY/Channel.ML src/HOL/UNITY/Common.ML src/HOL/UNITY/Common.thy src/HOL/UNITY/Handshake.ML src/HOL/UNITY/Lift.ML src/HOL/UNITY/Lift.thy src/HOL/UNITY/Mutex.ML src/HOL/UNITY/SubstAx.ML src/HOL/UNITY/SubstAx.thy src/HOL/UNITY/Token.ML src/HOL/UNITY/Token.thy src/HOL/UNITY/Traces.ML src/HOL/UNITY/UNITY.ML src/HOL/UNITY/WFair.ML src/HOL/UNITY/WFair.thy

1998-08-06 nipkow [Thu, 06 Aug 1998 14:04:49 +0200] rev 5276
Simplified proof!!
src/HOL/Lambda/InductTermi.ML

1998-08-06 nipkow [Thu, 06 Aug 1998 12:52:03 +0200] rev 5275
*** empty log message ***
NEWS

1998-08-06 nipkow [Thu, 06 Aug 1998 12:48:21 +0200] rev 5274
Lemma renamed in HOL.
src/HOLCF/IOA/NTP/Impl.ML

1998-08-06 nipkow [Thu, 06 Aug 1998 12:46:38 +0200] rev 5273
Added macro `termi'
src/HOL/Induct/Acc.thy

1998-08-06 nipkow [Thu, 06 Aug 1998 12:46:18 +0200] rev 5272
New lemmas in List and Lambda in IsaMakefile
src/HOL/IsaMakefile src/HOL/List.ML

1998-08-06 nipkow [Thu, 06 Aug 1998 12:45:28 +0200] rev 5271
Removed duplicate thms (see comment to Arith.ML)
src/HOL/Real/PNat.ML

1998-08-06 nipkow [Thu, 06 Aug 1998 12:45:02 +0200] rev 5270
Removed duplicate thms:
less_imp_add_less = trans_less_add1
le_imp_add_le = trans_le_add1
src/HOL/Arith.ML

1998-08-06 nipkow [Thu, 06 Aug 1998 12:44:07 +0200] rev 5269
Removed comments.
src/HOL/Lambda/InductTermi.ML