2000-06-22 wenzelm [Thu, 22 Jun 2000 23:04:34 +0200] rev 9108
bind_thm(s);
src/HOL/Datatype.ML src/HOL/Divides.ML src/HOL/Finite.ML src/HOL/Fun.ML src/HOL/Integ/Bin.ML src/HOL/Integ/IntDef.ML src/HOL/Integ/IntDiv.ML src/HOL/Integ/NatBin.ML src/HOL/List.ML src/HOL/Nat.ML src/HOL/NatDef.ML src/HOL/Real/Hyperreal/Filter.ML src/HOL/Real/Hyperreal/HyperDef.ML src/HOL/Real/Hyperreal/Zorn.ML src/HOL/Real/PNat.ML src/HOL/Real/PRat.ML src/HOL/Real/PReal.ML src/HOL/Real/ROOT.ML src/HOL/Real/RealBin.ML src/HOL/Real/RealDef.ML src/HOL/Relation.ML src/HOL/Set.ML src/HOL/Sum.ML src/HOL/Trancl.ML src/HOL/Univ.ML src/HOL/WF.ML src/HOL/WF_Rel.ML

2000-06-22 paulson [Thu, 22 Jun 2000 11:37:13 +0200] rev 9107
removed some finiteness conditions from bag_of/sublist theorems
src/HOL/UNITY/AllocBase.ML

2000-06-22 paulson [Thu, 22 Jun 2000 11:36:08 +0200] rev 9106
working proofs of the basic merge and distributor properties
src/HOL/UNITY/AllocImpl.ML

2000-06-22 paulson [Thu, 22 Jun 2000 11:35:28 +0200] rev 9105
fixed the merge spec (NbT -> Nclients) and added the distributor spec
src/HOL/UNITY/AllocImpl.thy

2000-06-22 paulson [Thu, 22 Jun 2000 11:34:48 +0200] rev 9104
new thoerem Always_Follows2; renamed Always_Follows -> Always_Follows1
src/HOL/UNITY/Follows.ML

2000-06-21 wenzelm [Wed, 21 Jun 2000 20:38:25 +0200] rev 9103
added with_paths;
src/Pure/Thy/thy_load.ML

2000-06-21 wenzelm [Wed, 21 Jun 2000 18:14:28 +0200] rev 9102
fixed deps;
src/HOL/Lambda/Eta.thy src/HOL/Lambda/InductTermi.thy src/HOL/Lambda/ListApplication.thy src/HOL/Lambda/ListOrder.thy

2000-06-21 wenzelm [Wed, 21 Jun 2000 18:09:09 +0200] rev 9101
fixed deps;
src/HOL/Induct/Acc.thy src/HOL/Induct/Comb.thy src/HOL/Induct/LFilter.thy src/HOL/Induct/Perm.thy src/HOL/Induct/PropLog.ML src/HOL/Induct/PropLog.thy src/HOL/IsaMakefile

2000-06-21 wenzelm [Wed, 21 Jun 2000 15:58:23 +0200] rev 9100
fixed deps;
src/HOL/ex/ROOT.ML src/HOL/ex/set.ML src/HOL/ex/set.thy

2000-06-21 paulson [Wed, 21 Jun 2000 10:34:33 +0200] rev 9099
new theorems lepoll_Ord_imp_eqpoll, lesspoll_imp_eqpoll, lesspoll_nat_is_Finite
src/ZF/Cardinal.ML