src/HOL/IsaMakefile
2003-12-23 paulson 2003-12-23 tidying up hcomplex arithmetic
2003-12-22 paulson 2003-12-22 converted Complex/NSComplex to Isar script
2003-12-22 paulson 2003-12-22 moving HyperArith0.ML to other theories
2003-12-17 paulson 2003-12-17 converted Hyperreal/HyperDef to Isar script
2003-12-16 paulson 2003-12-16 converted Hyperreal/HyperOrd to new-style theory
2003-12-10 paulson 2003-12-10 combining Real/{RealArith0,real_arith}.ML
2003-12-10 paulson 2003-12-10 Moving some theorems from Real/RealArith0.ML
2003-12-04 paulson 2003-12-04 further simplifications of the integer development; converting more .ML files to Isar scripts
2003-12-04 paulson 2003-12-04 Tidying of the integer development; towards removing the abel_cancel simproc
2003-11-28 paulson 2003-11-28 conversion of some Real theories to Isar scripts
2003-11-27 paulson 2003-11-27 Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files. New theorems for Ring_and_Field. Fixing affected proofs.
2003-11-25 paulson 2003-11-25 More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas to Isar script.
2003-11-24 paulson 2003-11-24 conversion of integers to use Ring_and_Field; new lemmas for Ring_and_Field
2003-11-21 paulson 2003-11-21 HOL: installation of Ring_and_Field as the basis for Naturals and Reals
2003-11-20 paulson 2003-11-20 conversion of Integ/Int_lemmas.ML to Isar script
2003-11-18 paulson 2003-11-18 conversion of ML to Isar scripts
2003-10-22 paulson 2003-10-22 InductiveInvariant_examples illustrates advanced recursive function definitions
2003-10-08 paulson 2003-10-08 Merging of ex/cla.ML and ex/mesontest.ML to ex/Classical.thy
2003-09-23 paulson 2003-09-23 new session HOL-SET-Protocol
2003-09-04 paulson 2003-09-04 conversion of HOL/Auth/KerberosIV to new-style theory
2003-08-15 paulson 2003-08-15 A document for UNITY
2003-08-12 paulson 2003-08-12 ZhouGollmann: new example (fair non-repudiation protocol)
2003-07-24 paulson 2003-07-24 new theory Library/NatPair
2003-07-17 skalberg 2003-07-17 Added package for definition by specification.
2003-07-03 paulson 2003-07-03 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
2003-07-03 paulson 2003-07-03 converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
2003-07-03 paulson 2003-07-03 Conversion of UNITY/Comp/Priority.thy to a linear Isar script
2003-06-26 nipkow 2003-06-26 *** empty log message ***
2003-06-24 berghofe 2003-06-24 Added new theories StrongNorm and WeakNorm to Lambda example.
2003-05-26 kleing 2003-05-26 set HOL_PROOF_OBJECTS in settings, not makefile (makes override in user settings possible) switched off by default
2003-05-24 kleing 2003-05-24 fixed
2003-05-23 kleing 2003-05-23 make it possible to switch off proof objects for HOL image
2003-05-14 schirmer 2003-05-14 Added Bali to test
2003-05-14 kleing 2003-05-14 use proof objects for HOL by default
2003-05-14 nipkow 2003-05-14 *** empty log message ***
2003-05-08 paulson 2003-05-08 new theory Complex_Main as basis for analysis developments
2003-05-08 kleing 2003-05-08 -> HOL-Complex-HahnBanach in clean target
2003-05-08 paulson 2003-05-08 removed obsolete references to HOL-Real
2003-05-07 kleing 2003-05-07 fixed HOL-Real-HahnBanach (-> HOL-Complex-HahnBanach)
2003-05-06 paulson 2003-05-06 removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
2003-05-06 kleing 2003-05-06 fixed missing -g true for HOL-Auth
2003-05-05 paulson 2003-05-05 new directory Complex
2003-05-02 ballarin 2003-05-02 HOL-Algebra complete for release Isabelle2003 (modulo section headers).
2003-05-01 paulson 2003-05-01 moving Bij.thy from GroupTheory to Algebra
2003-04-30 ballarin 2003-04-30 HOL-Algebra: new dependencies.
2003-04-26 paulson 2003-04-26 converting more HOL-Auth to new-style theories
2003-04-25 paulson 2003-04-25 Auth: certified email protocol
2003-04-11 webertj 2003-04-11 Map.ML integrated into Map.thy
2003-04-09 paulson 2003-04-09 Removal of Summation theory
2003-03-25 berghofe 2003-03-25 Added decision procedure for Presburger arithmetic.
2003-03-23 nipkow 2003-03-23 *** empty log message ***
2003-03-21 paulson 2003-03-21 quadratic reciprocity files
2003-03-18 paulson 2003-03-18 moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them to the new Group setup. Deleted Ring, Module from GroupTheory Minor UNITY changes
2003-03-11 nipkow 2003-03-11 *** empty log message ***
2003-03-10 paulson 2003-03-10 New theory ProgressSets. Definition of closure sets
2003-03-06 paulson 2003-03-06 new UNITY examples theory
2003-02-18 paulson 2003-02-18 new theory Transformers: Meier-Sanders non-interference theory
2003-01-31 paulson 2003-01-31 conversion to new-style theories and tidying
2003-01-30 paulson 2003-01-30 conversion of UNITY theories to new-style
2003-01-30 paulson 2003-01-30 converting more UNITY theories to new-style