src/HOL/IsaMakefile
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
2003-01-29 paulson 2003-01-29 converted more UNITY theories to new-style
2003-01-29 paulson 2003-01-29 converting UNITY to new-style theories
2003-01-27 kleing 2003-01-27 fixed missing UNITY files
2003-01-24 paulson 2003-01-24 Partial conversion of UNITY to Isar new-style theories
2003-01-08 nipkow 2003-01-08 New files in Hoare/
2002-12-11 ballarin 2002-12-11 HOL/GroupTheory/Summation.thy added: summation operator for abelian groups.
2002-11-28 ballarin 2002-11-28 HOL-Algebra partially ported to Isar.
2002-11-13 berghofe 2002-11-13 Added inductive_realizer.
2002-11-09 kleing 2002-11-09 Hoare.ML -> hoare.ML
2002-11-06 nipkow 2002-11-06 Hoare.ML -> hoare.ML
2002-11-05 kleing 2002-11-05 two new Bali files
2002-10-28 nipkow 2002-10-28 conversion ML -> thy
2002-10-23 streckem 2002-10-23 Added compiler
2002-09-27 paulson 2002-09-27 New theory GroupTheory/Module.thy of modules
2002-09-26 paulson 2002-09-26 Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML (which is automatically loaded with Int.thy) on case-insensitive filesystems.
2002-09-26 paulson 2002-09-26 Converted Fun to Isar style. Moved Pi, funcset, restrict from Fun.thy to Library/FuncSet.thy. Renamed constant "Fun.op o" to "Fun.comp"
2002-09-25 nipkow 2002-09-25 Int.thy -> int.thy
2002-08-31 paulson 2002-08-31 converted Hyperreal/Zorn to Isar format and moved to Library
2002-08-23 nipkow 2002-08-23 Added div+mod cancelling simproc
2002-08-21 paulson 2002-08-21 Frederic Blanqui's new "guard" examples
2002-08-08 wenzelm 2002-08-08 tuned deps;
2002-08-07 berghofe 2002-08-07 Added file Tools/datatype_realizer.ML
2002-08-05 berghofe 2002-08-05 Removed theory NatDef.
2002-07-21 berghofe 2002-07-21 Added theory for setting up program extraction.
2002-06-19 kleing 2002-06-19 LBV instantiantion refactored, streamlined
2002-06-03 nipkow 2002-06-03 Added ex/MergeSort
2002-05-28 paulson 2002-05-28 conversion of IntDiv.thy to Isar format
2002-05-17 nipkow 2002-05-17 Turned into Isar theories.
2002-05-15 nipkow 2002-05-15 Divides.ML -> Divides_lemmas.ML Converted Divides.thy to Isar.
2002-05-10 nipkow 2002-05-10 *** empty log message ***
2002-05-10 nipkow 2002-05-10 added dep on IMP/Compiler0
2002-05-08 paulson 2002-05-08 some ex files converted to Isar
2002-04-04 paulson 2002-04-04 conversion of Induct/{Slist,Sexp} to Isar scripts
2002-04-02 paulson 2002-04-02 conversion of some HOL/Induct proof scripts to Isar
2002-03-14 paulson 2002-03-14 removed ex/set.ML
2002-03-06 wenzelm 2002-03-06 tuned;
2002-03-06 wenzelm 2002-03-06 added HOL-Hyperreal-ex;
2002-03-05 prensani 2002-03-05 Target HoareParallel in IsaMakefile
2002-03-02 wenzelm 2002-03-02 temporarily disabled HoareParallel target;
2002-03-01 prensani 2002-03-01 Completed annonce of HoareParallel
2002-02-26 kleing 2002-02-26 introduces SystemClasses and BVExample
2002-02-26 wenzelm 2002-02-26 Isar_examples/W_correct moved to W0;
2002-02-21 wenzelm 2002-02-21 theory Option has been assimilated by Datatype;
2002-02-21 kleing 2002-02-21 new MicroJava document
2002-02-16 wenzelm 2002-02-16 converted/deleted equalities.ML, mono.ML, subset.ML (see Set.thy);
2002-02-05 wenzelm 2002-02-05 moved SVC stuff to ex;
2002-01-28 schirmer 2002-01-28 Bali added
2002-01-18 wenzelm 2002-01-18 fixed document setup of HOL-Library;
2002-01-17 nipkow 2002-01-17 Lex dependencies modified
2002-01-13 wenzelm 2002-01-13 added HOL/Real/document/root.tex;
2002-01-13 wenzelm 2002-01-13 Real/Complex_Numbers.thy;
2002-01-09 wenzelm 2002-01-09 converted theory Transitive_Closure;
2002-01-08 wenzelm 2002-01-08 HOL-Hyperreal produces an image (again);
2001-12-19 wenzelm 2001-12-19 HOL/IMP: include session graph;
2001-12-16 kleing 2001-12-16 MicroJava exception merge
2001-12-10 berghofe 2001-12-10 Added new files (code generator and examples).
2001-12-09 kleing 2001-12-09 HOL/IMP converted to Isar
2001-12-06 wenzelm 2001-12-06 include session graph;