2002-07-11 nipkow [Thu, 11 Jul 2002 09:31:01 +0200] rev 13344
*** empty log message ***
NEWS

2002-07-11 nipkow [Thu, 11 Jul 2002 09:17:01 +0200] rev 13343
*** empty log message ***
src/HOL/Lambda/Commutation.thy src/HOL/Relation.thy

2002-07-10 berghofe [Wed, 10 Jul 2002 18:39:15 +0200] rev 13342
expand_proof now also takes an optional term describing the proposition
of the theorem to be expanded (to avoid problems with different theorems
having the same names).
src/Pure/Proof/reconstruct.ML

2002-07-10 berghofe [Wed, 10 Jul 2002 18:37:51 +0200] rev 13341
- Moved abs_def to drule.ML
- elim_defs now takes a boolean argument which controls the automatic
expansion of theorems mentioning constants whose definitions are
eliminated
src/Pure/Proof/proof_rewrite_rules.ML

2002-07-10 berghofe [Wed, 10 Jul 2002 18:35:34 +0200] rev 13340
Simplified proof of induction rule for datatypes involving function types.
src/HOL/Tools/datatype_package.ML src/HOL/Tools/datatype_prop.ML src/HOL/Tools/datatype_rep_proofs.ML

2002-07-10 paulson [Wed, 10 Jul 2002 16:54:07 +0200] rev 13339
Fixed quantified variable name preservation for ball and bex (bounded quants)
Requires tweaking of other scripts. Also routine tidying.
src/ZF/AC/AC16_WO4.thy src/ZF/AC/AC16_lemmas.thy src/ZF/AC/AC17_AC1.thy src/ZF/AC/AC18_AC19.thy src/ZF/AC/Cardinal_aux.thy src/ZF/AC/DC.thy src/ZF/AC/HH.thy src/ZF/AC/Hartog.thy src/ZF/AC/WO1_WO7.thy src/ZF/AC/WO2_AC16.thy src/ZF/AC/WO6_WO1.thy src/ZF/Coind/ECR.thy src/ZF/Coind/Map.thy src/ZF/Coind/Types.thy src/ZF/Coind/Values.thy src/ZF/Constructible/Datatype_absolute.thy src/ZF/Constructible/Formula.thy src/ZF/Constructible/L_axioms.thy src/ZF/Constructible/ROOT.ML src/ZF/Constructible/Relative.thy src/ZF/Constructible/Separation.thy src/ZF/Constructible/WF_absolute.thy src/ZF/Constructible/WFrec.thy src/ZF/Constructible/Wellorderings.thy src/ZF/Induct/Multiset.ML src/ZF/Induct/Primrec.thy src/ZF/Integ/IntDiv.ML src/ZF/IsaMakefile src/ZF/List.thy src/ZF/OrdQuant.thy src/ZF/Order.thy src/ZF/OrderType.thy src/ZF/Resid/Confluence.thy src/ZF/Resid/Redex.thy src/ZF/Resid/Reduction.thy src/ZF/Resid/Residuals.thy src/ZF/Resid/Substitution.thy src/ZF/UNITY/Comp.ML src/ZF/UNITY/GenPrefix.ML src/ZF/UNITY/Guar.ML src/ZF/UNITY/ListPlus.ML src/ZF/UNITY/Union.ML src/ZF/ZF.ML src/ZF/ex/Commutation.thy src/ZF/ex/LList.thy src/ZF/ex/Limit.thy src/ZF/ex/Primes.thy src/ZF/ex/Ramsey.thy src/ZF/ex/misc.thy

2002-07-10 nipkow [Wed, 10 Jul 2002 16:07:52 +0200] rev 13338
*** empty log message ***
doc-src/TutorialI/IsarOverview/Isar/Logic.thy

2002-07-10 schirmer [Wed, 10 Jul 2002 15:07:02 +0200] rev 13337
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
src/HOL/Bali/AxCompl.thy src/HOL/Bali/AxSem.thy src/HOL/Bali/AxSound.thy src/HOL/Bali/Eval.thy src/HOL/Bali/Evaln.thy src/HOL/Bali/ROOT.ML src/HOL/Bali/State.thy src/HOL/Bali/Table.thy src/HOL/Bali/Term.thy src/HOL/Bali/Trans.thy src/HOL/Bali/TypeSafe.thy src/HOL/Bali/WellType.thy

2002-07-10 wenzelm [Wed, 10 Jul 2002 14:51:18 +0200] rev 13336
tuned add_thmss;
beginnings of locale predicates;
src/Pure/Isar/locale.ML

2002-07-10 wenzelm [Wed, 10 Jul 2002 14:50:08 +0200] rev 13335
tuned Locale.add_thmss;
src/Pure/Isar/proof.ML