src/HOL/IsaMakefile
Tue, 10 Jun 2008 19:15:20 +0200 wenzelm added HOL/Tools/induct_tacs.ML;
Tue, 10 Jun 2008 15:30:06 +0200 haftmann major refactorings in code generator modules
Sun, 01 Jun 2008 17:39:21 +0200 urbanc new example
Tue, 13 May 2008 09:14:07 +0200 krauss fixed makefile
Fri, 25 Apr 2008 15:30:33 +0200 krauss Merged theories about wellfoundedness into one: Wellfounded.thy
Tue, 22 Apr 2008 10:31:15 +0200 haftmann dropped theory PreList
Tue, 22 Apr 2008 08:33:21 +0200 haftmann added theory Sublist_Order
Wed, 16 Apr 2008 17:40:59 +0200 wenzelm removed unused TLA/Memory/MIParameters.thy;
Tue, 08 Apr 2008 20:14:36 +0200 krauss fixed makefiles
Thu, 20 Mar 2008 12:01:10 +0100 haftmann added theory Library/Enum.thy
Fri, 14 Mar 2008 19:57:12 +0100 nipkow Added lemmas
Wed, 12 Mar 2008 19:38:14 +0100 haftmann separated Random.thy from Quickcheck.thy
Fri, 07 Mar 2008 13:53:01 +0100 haftmann canonical order on option type
Tue, 04 Mar 2008 13:35:45 +0100 urbanc added new example
Mon, 03 Mar 2008 14:03:19 +0100 krauss new theory of red-black trees, an efficient implementation of finite maps.
Wed, 27 Feb 2008 21:41:08 +0100 haftmann added theories for imperative HOL
Wed, 27 Feb 2008 14:39:49 +0100 chaieb HOL/Dense_Linear_Order.thy moved to Library ; resulting dependencies updated
Mon, 25 Feb 2008 12:05:58 +0100 chaieb Added dependency of Library on Pocklington.thy
Mon, 25 Feb 2008 11:26:59 +0100 chaieb Included theories Library/Univ_Poly.thy and Complex/Fundamental_Theorem_Algebra.thy ; Theory Hyperreal/Poly.thy Removed
Wed, 20 Feb 2008 23:14:59 +0100 wenzelm removed ex/NBE.thy;
Fri, 25 Jan 2008 14:53:56 +0100 haftmann distinguished examples for Efficient_Nat.thy
Tue, 15 Jan 2008 16:19:23 +0100 haftmann joined theories IntDef, Numeral, IntArith to theory Int
Wed, 02 Jan 2008 15:14:15 +0100 haftmann improved evaluation mechanism
Thu, 20 Dec 2007 14:33:40 +0100 wenzelm moved Pure/General/random_word.ML to Tools/random_word.ML;
Thu, 20 Dec 2007 12:02:46 +0100 wenzelm updated HOL-Nominal-Examples deps;
Tue, 11 Dec 2007 10:23:05 +0100 haftmann joined EvenOdd theory with Parity
Fri, 07 Dec 2007 10:59:03 +0100 krauss Adding "ex/Induction_Scheme.thy" to tests
Thu, 06 Dec 2007 15:10:09 +0100 haftmann added new primrec package
Wed, 05 Dec 2007 14:16:15 +0100 haftmann dropped Classpackage.thy
Tue, 13 Nov 2007 10:59:26 +0100 berghofe Added new program extraction examples.
Tue, 06 Nov 2007 22:50:39 +0100 wenzelm activated HOL-SizeChange;
Tue, 06 Nov 2007 20:27:33 +0100 wenzelm removed dependencies on Size_Change_Termination from HOL-Library;
Tue, 06 Nov 2007 17:44:53 +0100 krauss moved stuff about size change termination to its own session
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:
less more (0) -300 -100 -60 tip