src/HOL/IsaMakefile
Thu, 19 Feb 2009 12:03:31 -0800 huffman add formalization of a type of integers mod 2 to Library
Thu, 19 Feb 2009 09:42:23 -0800 huffman new theory of real inner product spaces
Wed, 18 Feb 2009 20:14:45 -0800 huffman move Polynomial.thy to Library
Wed, 18 Feb 2009 19:51:39 -0800 huffman move FrechetDeriv.thy to Library
Wed, 18 Feb 2009 19:32:26 -0800 huffman split polynomial-related stuff from Deriv.thy into Library/Poly_Deriv.thy
Fri, 13 Feb 2009 09:54:47 +0100 nipkow Moved Nat_Int_Bij into Library
Thu, 12 Feb 2009 18:14:43 +0100 nipkow Moved FTA into Lib and cleaned it up a little.
Wed, 11 Feb 2009 10:51:07 +0100 nipkow Moved Order_Relation into Library and moved some of it into Relation.
Mon, 09 Feb 2009 17:21:46 +0000 chaieb added Determinants to Library
Mon, 09 Feb 2009 17:09:18 +0000 chaieb added Euclidean_Space and Glbs to Library
Mon, 09 Feb 2009 11:15:13 +0000 chaieb Added HOL/Library/Finite_Cartesian_Product.thy to Library
Fri, 06 Feb 2009 15:15:32 +0100 haftmann session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
Fri, 06 Feb 2009 00:13:15 +0000 chaieb fixed dependencies : Theory Dense_Linear_Order moved to Library
Thu, 05 Feb 2009 14:50:43 +0100 haftmann merged
Thu, 05 Feb 2009 14:14:02 +0100 haftmann moved Random.thy to Library
Thu, 05 Feb 2009 11:49:15 +0100 hoelzl Add approximation method
Thu, 05 Feb 2009 11:45:15 +0100 hoelzl Added new Float theory and moved old Library/Float.thy to ComputeFloat
Tue, 03 Feb 2009 18:34:49 +0100 haftmann merged Big0
Tue, 03 Feb 2009 16:50:41 +0100 haftmann established session HOL-Reflection
Mon, 16 Feb 2009 12:27:30 +0100 wenzelm removed obsolete axclass manual and examples;
Mon, 02 Feb 2009 13:56:22 +0100 haftmann added Mapping.thy to Library
Fri, 30 Jan 2009 17:47:34 +0100 krauss fixed case
Fri, 30 Jan 2009 13:24:23 +0000 chaieb Added Formal_Power_Series_Examples to HOL-ex image
Thu, 29 Jan 2009 14:56:28 +0000 chaieb Inserted Formal_Power_Series.thy under Library
Wed, 28 Jan 2009 11:04:10 +0100 haftmann Reflection.thy now in HOL/Library
Mon, 26 Jan 2009 22:14:16 +0100 haftmann entry point for Word library now named Word
Sat, 17 Jan 2009 08:28:51 +0100 haftmann no document for HOL-Base
Fri, 16 Jan 2009 08:29:11 +0100 haftmann added HOL-Base image
Mon, 12 Jan 2009 22:18:51 -0800 huffman add Polynomial.thy to makefile
Thu, 08 Jan 2009 17:10:41 +0100 haftmann split of Imperative_HOL theories from HOL-Library
Mon, 29 Dec 2008 14:08:08 +0100 haftmann adapted HOL source structure to distribution layout
Sat, 27 Dec 2008 17:35:00 +0100 krauss renamed LexOrds.thy to Termination.thy; examples for sizechange method
Tue, 16 Dec 2008 08:46:07 +0100 krauss method "sizechange" proves termination of functions; added more infrastructure for termination proofs
Mon, 15 Dec 2008 10:19:02 +0100 nipkow merged
Thu, 11 Dec 2008 08:52:50 +0100 nipkow Testfile for Stefan's code generator
Mon, 15 Dec 2008 09:58:45 +0100 haftmann moved value.ML to src/Tools
Wed, 10 Dec 2008 10:23:47 +0100 nipkow moved ContNotDenum into Library
Wed, 03 Dec 2008 15:58:44 +0100 haftmann made repository layout more coherent with logical distribution structure; stripped some $Id$s
Sat, 29 Nov 2008 13:39:23 +0100 nipkow new file float_syntax.ML
Mon, 17 Nov 2008 21:13:48 +0100 wenzelm removed Induct/Mutil.thy -- the file has been moved to AFP;
Sat, 15 Nov 2008 21:31:15 +0100 wenzelm clean: added HOL-Main;
Thu, 13 Nov 2008 15:59:33 +0100 haftmann moved assert to Heap_Monad.thy
Tue, 21 Oct 2008 21:18:54 +0200 berghofe Added nominal_inductive2.ML
Fri, 17 Oct 2008 10:39:39 +0200 wenzelm reactivated HOL-Matrix;
Thu, 16 Oct 2008 17:52:54 +0200 ballarin Removed ex/Locales.thy.
Tue, 14 Oct 2008 16:01:36 +0200 wenzelm renamed AtpThread to AtpWrapper;
Sat, 04 Oct 2008 16:05:09 +0200 wenzelm replaced ISATOOL by ISABELLE_TOOL;
Fri, 03 Oct 2008 16:37:09 +0200 wenzelm version of sledgehammer using threads instead of processes, misc cleanup;
Fri, 03 Oct 2008 15:20:33 +0200 wenzelm removed old/unused setup of raw ATP oracles;
Mon, 29 Sep 2008 12:31:58 +0200 haftmann separate HOL-Main image
Sun, 28 Sep 2008 14:46:51 +0200 wenzelm HOL no longer depends on HOL-Plain;
Sat, 27 Sep 2008 14:26:06 +0200 wenzelm HOL_USEDIR_OPTIONS no longer applies to HOL-Plain (main HOL is rebuilt from Pure);
Mon, 22 Sep 2008 23:04:35 +0200 berghofe Added coherent logic prover.
Mon, 22 Sep 2008 13:55:59 +0200 haftmann different session branches for HOL-Plain vs. Plain
Tue, 16 Sep 2008 16:13:06 +0200 haftmann moved term_of syntax to separate theory
Tue, 16 Sep 2008 09:21:22 +0200 haftmann generic value command
Wed, 03 Sep 2008 12:11:28 +0200 nipkow removed ex/Puzzle
Tue, 02 Sep 2008 22:37:20 +0200 nipkow Replaced Library/NatPair by Nat_Int_Bij.
Thu, 28 Aug 2008 22:09:20 +0200 haftmann restructured and split code serializer module
Wed, 27 Aug 2008 12:01:59 +0200 haftmann added HOL/ex/Numeral.thy
less more (0) -300 -100 -60 tip