src/HOL/IsaMakefile
Mon, 05 Nov 2007 22:50:48 +0100 kleing add root.bib for Word document
Wed, 24 Oct 2007 19:21:39 +0200 wenzelm fixed HOL-Statespace for case-sensitive file-system;
Wed, 24 Oct 2007 18:36:09 +0200 schirmer added Statespace library
Fri, 12 Oct 2007 08:21:09 +0200 haftmann consolidated naming conventions for code generator theories
Mon, 08 Oct 2007 22:03:25 +0200 haftmann integrated FixedPoint into Inductive
Mon, 08 Oct 2007 07:09:29 +0200 urbanc changed VC-Compatible to VC_Compatible
Mon, 08 Oct 2007 05:27:52 +0200 urbanc added the two new examples from Nominal to the build process
Thu, 04 Oct 2007 14:42:47 +0200 wenzelm moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
Sat, 29 Sep 2007 10:40:12 +0200 kleing Added target for proof term sessions (those that need -p 2)
Tue, 25 Sep 2007 12:16:08 +0200 haftmann datatype interpretators for size and datatype_realizer
Tue, 18 Sep 2007 18:05:34 +0200 wenzelm moved Tools/integer.ML to Pure/General/integer.ML;
Tue, 18 Sep 2007 07:46:00 +0200 haftmann introduced generic concepts for theory interpretators
Tue, 18 Sep 2007 07:36:38 +0200 haftmann separated code for inductive sequences from inductive_codegen.ML
Tue, 18 Sep 2007 06:21:40 +0200 nipkow sorting
Sun, 16 Sep 2007 21:04:44 +0200 wenzelm added Induct/Common_Patterns.thy;
Thu, 06 Sep 2007 11:52:13 +0200 berghofe - New theories Lambda/NormalForm and Lambda/Standardization
Wed, 29 Aug 2007 13:58:00 +0200 wenzelm added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
Wed, 29 Aug 2007 11:10:28 +0200 wenzelm removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
Tue, 28 Aug 2007 20:13:47 +0200 huffman revert to Word library version from 2007/08/20
Tue, 28 Aug 2007 18:24:34 +0200 berghofe codegen.ML is now loaded in Pure again.
Tue, 28 Aug 2007 03:56:24 +0200 huffman HOL-Word-Examples
Thu, 23 Aug 2007 16:47:16 +0200 huffman Word/BinInduct.thy
Wed, 22 Aug 2007 21:09:21 +0200 huffman removed Word/Size.thy;
Wed, 22 Aug 2007 16:54:43 +0200 huffman Word/WordBoolList.thy
Tue, 21 Aug 2007 00:24:10 +0200 wenzelm use HOL-ex later;
Mon, 20 Aug 2007 17:34:04 +0200 huffman Word/document/root.tex
Mon, 20 Aug 2007 04:34:31 +0200 kleing * HOL-Word:
Mon, 20 Aug 2007 00:22:18 +0200 kleing boolean algebras as locales and numbers as types by Brian Huffman
Sat, 18 Aug 2007 17:42:38 +0200 wenzelm converted ex/MT.ML;
Sat, 18 Aug 2007 13:32:28 +0200 wenzelm make HOL-ex earlier;
Wed, 15 Aug 2007 15:06:58 +0200 paulson combining the relevance filter with res_atp
Wed, 15 Aug 2007 08:57:39 +0200 haftmann updated code generator setup
Thu, 09 Aug 2007 15:52:42 +0200 haftmann re-eliminated Option.thy
Tue, 07 Aug 2007 09:38:44 +0200 haftmann split off theory Option for benefit of code generator
Fri, 03 Aug 2007 22:35:40 +0200 wenzelm reactivated Nominal/Examples/Class.thy;
Fri, 03 Aug 2007 16:28:18 +0200 wenzelm added dependency on Tools/Metis/metis.ML;
Thu, 02 Aug 2007 15:44:37 +0200 wenzelm converted Meson tests to proper theory;
Tue, 31 Jul 2007 22:21:18 +0200 wenzelm removed obsolete HOL/Real/ROOT.ML;
Tue, 31 Jul 2007 19:40:22 +0200 wenzelm added Tools/lin_arith.ML;
Tue, 31 Jul 2007 09:31:23 +0200 chaieb Added dependency on langford files in Tools/Qelim
Sun, 29 Jul 2007 14:29:50 +0200 wenzelm removed obsolete Tools/res_atpset.ML;
Fri, 20 Jul 2007 14:33:40 +0200 haftmann dropped Nat.ML legacy bindings
Thu, 19 Jul 2007 21:47:39 +0200 haftmann uniform naming conventions for CG theories
Wed, 11 Jul 2007 11:51:12 +0200 obua changed sources for HOL-Complex-Matrix
Wed, 11 Jul 2007 10:59:23 +0200 berghofe Added new package for inductive sets.
Mon, 09 Jul 2007 22:06:49 +0200 wenzelm HOL-Complex-Matrix: fixed deps -- sort of;
Thu, 05 Jul 2007 00:06:11 +0200 wenzelm added Tools/numeral.ML;
Tue, 03 Jul 2007 18:00:57 +0200 chaieb Dependency on reflection_data.ML to build HOL-ex
Fri, 29 Jun 2007 18:21:25 +0200 paulson bug fixes to proof reconstruction
Tue, 26 Jun 2007 13:01:48 +0200 nipkow added NBE
Mon, 25 Jun 2007 12:16:27 +0200 krauss removed "sum_tools.ML" in favour of BalancedTree
Thu, 21 Jun 2007 20:48:48 +0200 wenzelm moved quantifier elimination tools to Tools/Qelim/;
Thu, 21 Jun 2007 17:28:50 +0200 wenzelm renamed NatSimprocs.thy to Arith_Tools.thy;
Thu, 21 Jun 2007 15:42:07 +0200 wenzelm replaced Real/Ferrante-Rackoff tool by generic version in Main HOL;
Thu, 21 Jun 2007 13:23:33 +0200 paulson integration of Metis prover
Wed, 20 Jun 2007 23:19:17 +0200 wenzelm added Tools/metis_tools.ML;
Mon, 11 Jun 2007 18:26:44 +0200 chaieb Added dependency on file Groebner_Basis.thy
Mon, 11 Jun 2007 11:05:59 +0200 chaieb Added new files for Presburger (cooper_data.ML, cooper.ML) and deleted old unused ones cooper_dec, cooper_proof, reflected_cooper etc..
Wed, 06 Jun 2007 21:24:35 +0200 urbanc take out Class.thy again, because it does not yet compile cleanly
Wed, 06 Jun 2007 16:12:08 +0200 chaieb New Reflected Presburger added to HOL/ex
less more (0) -300 -100 -60 tip