2002-08-27 wenzelm [Tue, 27 Aug 2002 11:06:20 +0200] rev 13530
Thm.proof_of;
src/Pure/Proof/proof_syntax.ML src/Pure/Thy/thm_deps.ML

2002-08-27 wenzelm [Tue, 27 Aug 2002 11:06:07 +0200] rev 13529
check_goal: produce error instead of warning;
src/Pure/Isar/isar_thy.ML

2002-08-27 wenzelm [Tue, 27 Aug 2002 11:05:31 +0200] rev 13528
added proof_of;
src/Pure/thm.ML

2002-08-27 wenzelm [Tue, 27 Aug 2002 11:05:13 +0200] rev 13527
thms/axms_of_proof: proper handling of MinProof;
src/Pure/proofterm.ML

2002-08-27 wenzelm [Tue, 27 Aug 2002 11:04:27 +0200] rev 13526
result dependency output;
src/Pure/proof_general.ML

2002-08-27 wenzelm [Tue, 27 Aug 2002 11:04:00 +0200] rev 13525
dup_elim: improved error reporting;
src/Provers/classical.ML

2002-08-27 wenzelm [Tue, 27 Aug 2002 11:03:05 +0200] rev 13524
*** empty log message ***
src/HOL/Bali/AxCompl.thy src/HOL/Bali/DeclConcepts.thy src/HOL/Bali/Example.thy src/HOL/Bali/State.thy src/HOL/Bali/WellType.thy src/HOL/HoareParallel/RG_Hoare.thy src/HOL/Hyperreal/EvenOdd.ML src/HOL/IMP/Transition.thy src/HOL/IMPP/Hoare.ML src/HOL/Induct/LList.thy src/HOL/Integ/IntDiv.thy src/HOL/Isar_examples/ExprCompiler.thy src/HOL/MicroJava/BV/BVSpecTypeSafe.thy src/HOL/NanoJava/State.thy src/HOL/NumberTheory/BijectionRel.thy src/HOL/NumberTheory/Chinese.thy src/HOL/NumberTheory/EulerFermat.thy src/HOL/NumberTheory/IntPrimes.thy src/HOL/NumberTheory/WilsonRuss.thy src/HOL/Real/HahnBanach/FunctionNorm.thy src/HOLCF/FOCUS/Buffer_adm.ML src/HOLCF/Fix.ML src/HOLCF/IOA/ABP/Lemmas.ML src/HOLCF/IOA/NTP/Lemmas.ML src/HOLCF/IOA/ex/TrivEx.ML src/HOLCF/IOA/ex/TrivEx2.ML src/HOLCF/ex/loeckx.ML src/ZF/Cardinal.thy src/ZF/Epsilon.thy src/ZF/Finite.thy src/ZF/List.thy src/ZF/Nat.thy

2002-08-27 wenzelm [Tue, 27 Aug 2002 11:03:02 +0200] rev 13523
avoid duplicate fact bindings;
src/HOL/Auth/Guard/Guard_Shared.thy

2002-08-27 wenzelm [Tue, 27 Aug 2002 10:59:21 +0200] rev 13522
* Isar: preview of problems to finish 'show' now produce an error
NEWS

2002-08-24 paulson [Sat, 24 Aug 2002 18:53:43 +0200] rev 13521
conversion of ZF/IntDiv to Isar script
src/ZF/Integ/IntDiv.ML