2004-08-16 nipkow [Mon, 16 Aug 2004 14:22:27 +0200] rev 15131
New theory header syntax.
src/HOL/Complex/CLim.thy src/HOL/Complex/CSeries.thy src/HOL/Complex/CStar.thy src/HOL/Complex/Complex.thy src/HOL/Complex/ComplexBin.thy src/HOL/Complex/Complex_Main.thy src/HOL/Complex/NSCA.thy src/HOL/Complex/NSComplex.thy src/HOL/Datatype.thy src/HOL/Divides.thy src/HOL/Extraction.thy src/HOL/Finite_Set.thy src/HOL/Fun.thy src/HOL/Gfp.thy src/HOL/HOL.thy src/HOL/Hilbert_Choice.thy src/HOL/Hyperreal/EvenOdd.thy src/HOL/Hyperreal/Fact.thy src/HOL/Hyperreal/Filter.thy src/HOL/Hyperreal/HLog.thy src/HOL/Hyperreal/HSeries.thy src/HOL/Hyperreal/HTranscendental.thy src/HOL/Hyperreal/HyperArith.thy src/HOL/Hyperreal/HyperDef.thy src/HOL/Hyperreal/HyperNat.thy src/HOL/Hyperreal/HyperPow.thy src/HOL/Hyperreal/Hyperreal.thy src/HOL/Hyperreal/Integration.thy src/HOL/Hyperreal/Lim.thy src/HOL/Hyperreal/Log.thy src/HOL/Hyperreal/MacLaurin.thy src/HOL/Hyperreal/NSA.thy src/HOL/Hyperreal/NatStar.thy src/HOL/Hyperreal/NthRoot.thy src/HOL/Hyperreal/Poly.thy src/HOL/Hyperreal/SEQ.thy src/HOL/Hyperreal/Series.thy src/HOL/Hyperreal/Star.thy src/HOL/Hyperreal/Transcendental.thy src/HOL/Inductive.thy src/HOL/Infinite_Set.thy src/HOL/Integ/Equiv.thy src/HOL/Integ/IntArith.thy src/HOL/Integ/IntDef.thy src/HOL/Integ/IntDiv.thy src/HOL/Integ/NatBin.thy src/HOL/Integ/NatSimprocs.thy src/HOL/Integ/Numeral.thy src/HOL/Integ/Parity.thy src/HOL/Integ/Presburger.thy ...

2004-08-16 nipkow [Mon, 16 Aug 2004 14:21:54 +0200] rev 15130
*** empty log message ***
NEWS

2004-08-16 berghofe [Mon, 16 Aug 2004 12:29:09 +0200] rev 15129
Replaced `div and `mod in consts_code section by div and mod.
src/HOL/Integ/NatBin.thy

2004-08-14 webertj [Sat, 14 Aug 2004 16:27:56 +0200] rev 15128
bugfix in read_dimacs_cnf_file
src/HOL/Tools/sat_solver.ML

2004-08-12 ballarin [Thu, 12 Aug 2004 10:01:09 +0200] rev 15127
Disallowed "includes" in locale declarations.
NEWS src/Pure/Isar/isar_cmd.ML src/Pure/Isar/isar_syn.ML src/Pure/Isar/isar_thy.ML src/Pure/Isar/locale.ML src/Pure/Isar/outer_parse.ML src/Pure/Isar/proof.ML

2004-08-10 berghofe [Tue, 10 Aug 2004 19:10:39 +0200] rev 15126
Fixed bug in compile_clause that caused equality constraints
to be "forgotten".
src/HOL/Tools/inductive_codegen.ML

2004-08-09 webertj [Mon, 09 Aug 2004 15:27:27 +0200] rev 15125
warning for recursion over IDTs added
src/HOL/Tools/refute.ML

2004-08-09 nipkow [Mon, 09 Aug 2004 10:09:44 +0200] rev 15124
Aded a thm.
src/HOL/Finite_Set.thy

2004-08-06 chaieb [Fri, 06 Aug 2004 17:29:24 +0200] rev 15123
*** empty log message ***
src/HOL/Integ/cooper_proof.ML src/HOL/Tools/Presburger/cooper_proof.ML

2004-08-06 chaieb [Fri, 06 Aug 2004 17:19:50 +0200] rev 15122
proof_of_evalc corrected;
src/HOL/Integ/cooper_proof.ML src/HOL/Tools/Presburger/cooper_proof.ML