2004-08-18 nipkow [Wed, 18 Aug 2004 11:09:40 +0200] rev 15140
import -> imports
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-17 kleing [Tue, 17 Aug 2004 11:00:24 +0200] rev 15139
todo before next release
TODO

2004-08-17 kleing [Tue, 17 Aug 2004 10:49:52 +0200] rev 15138
improved wording course material
Admin/page/main-content/index.content

2004-08-17 kleing [Tue, 17 Aug 2004 01:20:29 +0200] rev 15137
include course material page
Admin/page/dist-content/docs.content Admin/page/main-content/docs.content Admin/page/main-content/index.content

2004-08-16 nipkow [Mon, 16 Aug 2004 19:47:01 +0200] rev 15136
Adapted text to new theory header syntax.
doc-src/TutorialI/Documents/Documents.thy doc-src/TutorialI/Documents/document/Documents.tex doc-src/TutorialI/ToyList/ToyList.thy doc-src/TutorialI/ToyList/document/ToyList.tex doc-src/TutorialI/ToyList2/ToyList1 doc-src/TutorialI/basics.tex

2004-08-16 nipkow [Mon, 16 Aug 2004 19:06:59 +0200] rev 15135
Added "import" and "begin"
etc/isar-keywords-ZF.el etc/isar-keywords.el

2004-08-16 aspinall [Mon, 16 Aug 2004 18:05:41 +0200] rev 15134
Experimental version supporting PGIP, merged with main branch with help from Makarius.
src/Pure/proof_general.ML

2004-08-16 aspinall [Mon, 16 Aug 2004 17:56:07 +0200] rev 15133
Experimental pgip_isar.xml file
lib/ProofGeneral/pgip_isar.xml

2004-08-16 nipkow [Mon, 16 Aug 2004 17:06:47 +0200] rev 15132
new theory header syntax.
src/Pure/Isar/isar_syn.ML src/Pure/Isar/thy_header.ML

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 ...