2003-08-29 ballarin [Fri, 29 Aug 2003 15:19:02 +0200] rev 14174
Methods rule_tac etc support static (Isar) contexts.
src/HOL/Bali/WellForm.thy src/HOL/HoareParallel/RG_Examples.thy src/HOL/MicroJava/Comp/CorrComp.thy src/HOL/MicroJava/Comp/CorrCompTp.thy src/HOL/MicroJava/J/Conform.thy src/HOL/MicroJava/J/State.thy src/HOL/MicroJava/J/WellForm.thy src/HOL/NanoJava/Equivalence.thy src/HOL/NumberTheory/EulerFermat.thy src/HOL/NumberTheory/IntPrimes.thy src/HOL/Tools/datatype_package.ML src/Pure/Isar/args.ML src/Pure/Isar/method.ML src/Pure/Isar/proof_context.ML

2003-08-29 skalberg [Fri, 29 Aug 2003 13:18:45 +0200] rev 14173
Removed the extended digits again.
NEWS src/Pure/General/symbol.ML

2003-08-28 skalberg [Thu, 28 Aug 2003 02:00:16 +0200] rev 14172
Fixed typos.
NEWS

2003-08-28 skalberg [Thu, 28 Aug 2003 01:56:40 +0200] rev 14171
Extended the notion of letter and digit, such that now one may use greek,
gothic, euler, or calligraphic letters as normal letters.
NEWS lib/Tools/fixgreek lib/scripts/fixgreek.pl src/HOL/Bali/Decl.thy src/HOL/Bali/State.thy src/HOL/Bali/Type.thy src/HOL/MicroJava/J/TypeRel.thy src/HOL/NanoJava/TypeRel.thy src/HOLCF/FOCUS/Buffer.ML src/HOLCF/FOCUS/Fstream.thy src/HOLCF/ex/Stream.ML src/HOLCF/ex/Stream.thy src/Pure/General/symbol.ML src/ZF/AC.thy src/ZF/AC/AC15_WO6.thy src/ZF/AC/AC17_AC1.thy src/ZF/AC/AC18_AC19.thy src/ZF/AC/AC7_AC9.thy src/ZF/AC/AC_Equiv.thy src/ZF/AC/HH.thy src/ZF/Coind/Map.thy src/ZF/Constructible/AC_in_L.thy src/ZF/Constructible/Formula.thy src/ZF/Constructible/L_axioms.thy src/ZF/Constructible/Normal.thy src/ZF/Constructible/Reflection.thy src/ZF/Induct/Brouwer.thy src/ZF/OrderArith.thy src/ZF/UNITY/State.thy src/ZF/Zorn.thy src/ZF/equalities.thy src/ZF/ex/Limit.thy

2003-08-27 skalberg [Wed, 27 Aug 2003 18:22:34 +0200] rev 14170
Added skalberg to recepients, changed admin from kleing to berghofe.
Admin/isatest-check Admin/isatest-makedist

2003-08-27 skalberg [Wed, 27 Aug 2003 18:13:59 +0200] rev 14169
Converted to new style theories.
src/HOL/Gfp.ML src/HOL/Gfp.thy src/HOL/Lfp.ML src/HOL/Lfp.thy

2003-08-27 skalberg [Wed, 27 Aug 2003 18:13:39 +0200] rev 14168
Prepared for extended identifiers (\<alpha>, etc.)
src/HOL/Extraction.thy

2003-08-27 skalberg [Wed, 27 Aug 2003 10:11:30 +0200] rev 14167
Improved the error messages (slightly).
src/HOL/Tools/specification_package.ML

2003-08-26 skalberg [Tue, 26 Aug 2003 19:33:35 +0200] rev 14166
Cleaned up the code.
src/HOL/Tools/specification_package.ML

2003-08-26 skalberg [Tue, 26 Aug 2003 19:33:04 +0200] rev 14165
New specification syntax added (the specification may be split over
several properties).
doc-src/IsarRef/logics.tex