src/HOL/IsaMakefile
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
Tue, 05 Jun 2007 22:46:55 +0200 wenzelm added ex/Groebner_Examples.thy;
Tue, 05 Jun 2007 20:46:25 +0200 chaieb Added two examples in Complex/ex :Reflected QE for linear real arith and QE for mixed integer real linear arithmetic
Tue, 05 Jun 2007 16:26:04 +0200 wenzelm Semiring normalization and Groebner Bases.
Tue, 05 Jun 2007 15:16:08 +0200 haftmann merged Code_Generator.thy into HOL.thy
Tue, 05 Jun 2007 09:56:19 +0200 urbanc included Class.thy in the compiling process for Nominal/Examples
Sun, 03 Jun 2007 23:16:41 +0200 wenzelm HOL-ex: tuned deps;
Fri, 01 Jun 2007 23:33:49 +0200 webertj tuned
Fri, 01 Jun 2007 23:21:40 +0200 webertj some tests for arith added
Fri, 01 Jun 2007 22:09:16 +0200 nipkow Moved list comprehension into List
Thu, 31 May 2007 20:55:31 +0200 wenzelm moved IsaPlanner from Provers to Tools;
Thu, 31 May 2007 18:16:52 +0200 wenzelm moved Integ files to canonical place;
Thu, 31 May 2007 13:18:52 +0200 wenzelm moved TFL files to canonical place;
Thu, 31 May 2007 12:06:31 +0200 wenzelm moved Integ files to canonical place;
Thu, 31 May 2007 10:17:23 +0200 urbanc included new example in the compiling process
Fri, 25 May 2007 18:08:34 +0200 nipkow Added List_Comprehension
Fri, 25 May 2007 05:18:56 +0200 urbanc took out Class.thy from the compiling process until memory problems are solved
Tue, 22 May 2007 05:07:48 +0200 huffman remove obsolete CSeries.thy
Fri, 18 May 2007 09:16:57 +0200 haftmann dropped word_setup.ML
Thu, 17 May 2007 23:03:47 +0200 krauss updated
Tue, 15 May 2007 18:28:02 +0200 chaieb A verified theory for rational numbers representation and simple calculations;
Mon, 14 May 2007 12:52:56 +0200 haftmann reorganized float arithmetic
Sun, 13 May 2007 18:15:21 +0200 haftmann added modules rat.ML and int.ML
Wed, 09 May 2007 19:37:22 +0200 wenzelm removed Complex/ComplexBin.thy;
Sun, 06 May 2007 21:49:24 +0200 haftmann dropped HOL.ML
less more (0) -300 -100 -60 tip