1996-02-06 clasohm [Tue, 06 Feb 1996 12:27:17 +0100] rev 1478
expanded tabs
src/ZF/AC.thy src/ZF/AC/AC16_WO4.thy src/ZF/AC/AC18_AC19.thy src/ZF/AC/AC_Equiv.thy src/ZF/AC/DC.thy src/ZF/AC/HH.thy src/ZF/AC/Hartog.thy src/ZF/AC/OrdQuant.thy src/ZF/AC/Transrec2.thy src/ZF/AC/WO6_WO1.thy src/ZF/AC/first.thy src/ZF/AC/recfunAC16.thy src/ZF/Arith.thy src/ZF/Bool.thy src/ZF/Cardinal.thy src/ZF/CardinalArith.thy src/ZF/Cardinal_AC.thy src/ZF/Coind/BCR.thy src/ZF/Coind/Dynamic.thy src/ZF/Coind/ECR.thy src/ZF/Coind/Language.thy src/ZF/Coind/Map.thy src/ZF/Coind/Static.thy src/ZF/Coind/Types.thy src/ZF/Coind/Values.thy src/ZF/Epsilon.thy src/ZF/EquivClass.thy src/ZF/Finite.thy src/ZF/Fixedpt.thy src/ZF/IMP/Com.thy src/ZF/IMP/Denotation.thy src/ZF/IMP/Equiv.thy src/ZF/Let.thy src/ZF/List.thy src/ZF/Nat.thy src/ZF/Order.thy src/ZF/OrderArith.thy src/ZF/OrderType.thy src/ZF/Ordinal.thy src/ZF/Perm.thy src/ZF/QPair.thy src/ZF/QUniv.thy src/ZF/Rel.thy src/ZF/Resid/Confluence.thy src/ZF/Resid/Conversion.thy src/ZF/Resid/Cube.thy src/ZF/Resid/Redex.thy src/ZF/Resid/Reduction.thy src/ZF/Resid/Residuals.thy src/ZF/Resid/SubUnion.thy ...

1996-02-05 clasohm [Mon, 05 Feb 1996 21:33:14 +0100] rev 1477
expanded tabs
src/FOLP/FOLP.thy src/FOLP/IFOLP.thy src/FOLP/ex/Nat.thy src/FOLP/ex/Prolog.thy

1996-02-05 clasohm [Mon, 05 Feb 1996 21:29:06 +0100] rev 1476
expanded tabs; incorporated Konrad's changes
src/HOL/AxClasses/Lattice/OrdDefs.thy src/HOL/Hoare/Arith2.ML src/HOL/Hoare/Arith2.thy src/HOL/Hoare/Examples.thy src/HOL/Hoare/Hoare.thy src/HOL/IMP/Com.thy src/HOL/IMP/Denotation.thy src/HOL/IMP/Equiv.thy src/HOL/IMP/Hoare.thy src/HOL/IMP/VC.thy src/HOL/IOA/ABP/Abschannel.thy src/HOL/IOA/ABP/Abschannel_finite.thy src/HOL/IOA/ABP/Correctness.thy src/HOL/IOA/ABP/Receiver.thy src/HOL/IOA/ABP/Sender.thy src/HOL/IOA/NTP/Abschannel.thy src/HOL/IOA/meta_theory/IOA.thy src/HOL/Integ/Equiv.thy src/HOL/Integ/Integ.thy src/HOL/Lambda/Commutation.thy src/HOL/Lex/Auto.thy src/HOL/Lex/AutoChopper.thy src/HOL/Lex/Chopper.thy src/HOL/Lex/Prefix.thy src/HOL/MiniML/I.thy src/HOL/MiniML/MiniML.thy src/HOL/MiniML/Type.thy src/HOL/MiniML/W.thy src/HOL/Subst/AList.thy src/HOL/Subst/Setplus.thy src/HOL/Subst/Subst.thy src/HOL/Subst/UTLemmas.thy src/HOL/Subst/UTerm.ML src/HOL/Subst/UTerm.thy src/HOL/Subst/Unifier.thy src/HOL/ex/Acc.thy src/HOL/ex/BT.thy src/HOL/ex/InSort.thy src/HOL/ex/LList.thy src/HOL/ex/LexProd.thy src/HOL/ex/MT.thy src/HOL/ex/NatSum.thy src/HOL/ex/Perm.thy src/HOL/ex/PropLog.thy src/HOL/ex/Puzzle.thy src/HOL/ex/Qsort.thy src/HOL/ex/Rec.thy src/HOL/ex/SList.ML src/HOL/ex/SList.thy src/HOL/ex/Simult.ML ...

1996-02-05 clasohm [Mon, 05 Feb 1996 21:27:16 +0100] rev 1475
expanded tabs; renamed subtype to typedef;
incorporated Konrad's changes
src/HOL/Arith.ML src/HOL/Arith.thy src/HOL/Finite.thy src/HOL/Fun.thy src/HOL/Gfp.thy src/HOL/Lfp.thy src/HOL/List.thy src/HOL/Nat.ML src/HOL/Nat.thy src/HOL/Prod.thy src/HOL/Relation.thy src/HOL/Sexp.ML src/HOL/Sexp.thy src/HOL/Sum.thy src/HOL/Trancl.thy src/HOL/Univ.thy src/HOL/WF.ML src/HOL/WF.thy src/HOL/equalities.thy src/HOL/mono.thy src/HOL/subset.thy src/HOL/thy_syntax.ML src/HOL/typedef.ML

1996-02-05 clasohm [Mon, 05 Feb 1996 14:44:09 +0100] rev 1474
expanded tabs
src/CCL/CCL.thy src/CCL/Fix.thy src/CCL/Gfp.thy src/CCL/Hered.thy src/CCL/Lfp.thy src/CCL/Term.thy src/CCL/Trancl.thy src/CCL/Type.thy src/CCL/Wfd.thy src/CCL/ex/Flag.thy src/CCL/ex/List.thy src/CCL/ex/Nat.thy src/CCL/ex/Stream.thy src/CTT/Arith.thy src/CTT/Bool.thy src/LCF/LCF.thy src/LK/LK.thy src/Modal/Modal0.thy src/Modal/S4.thy src/Modal/S43.thy src/Modal/T.thy

1996-02-05 clasohm [Mon, 05 Feb 1996 13:44:28 +0100] rev 1473
expanded tabs
src/FOL/ex/List.thy src/FOL/ex/Nat.thy src/FOL/ex/Nat2.thy src/FOL/ex/Prolog.thy src/FOL/ex/foundn.ML

1996-02-02 clasohm [Fri, 02 Feb 1996 12:05:24 +0100] rev 1472
renamed subtype.ML to typedef.ML
src/HOL/Makefile

1996-02-01 nipkow [Thu, 01 Feb 1996 16:18:52 +0100] rev 1471
documented split_all_tac in HOL.
doc-src/Logics/HOL.tex

1996-02-01 clasohm [Thu, 01 Feb 1996 13:25:40 +0100] rev 1470
renamed subtype.ML to typedef.ML
src/HOL/ROOT.ML src/HOL/subtype.ML

1996-02-01 clasohm [Thu, 01 Feb 1996 12:08:43 +0100] rev 1469
fixed two little bugs
src/Tools/install_html.sh