src/HOL/ex/ROOT.ML
Thu, 11 Jun 2009 12:50:20 +0200 wenzelm theory Predicate_Compile_ex: enable quick_and_dirty for now, to make it work with internal cheat_tac invocations;
Tue, 02 Jun 2009 18:26:01 +0200 haftmann added Landau theory
Tue, 02 Jun 2009 15:53:07 +0200 haftmann tuned code generator test theories
Fri, 15 May 2009 16:39:17 +0200 haftmann dropped theory Term_Of_Syntax
Tue, 12 May 2009 21:17:47 +0200 haftmann split Predicate_Compile examples into separate theory
Fri, 27 Mar 2009 10:05:13 +0100 haftmann dropped toy example Code_Antiq
Mon, 23 Mar 2009 19:01:17 +0100 haftmann moved Imperative_HOL examples to Imperative_HOL/ex
Wed, 11 Mar 2009 08:45:47 +0100 haftmann moved Decision_Procs examples to Decision_Procs/ex
Sun, 08 Mar 2009 15:25:28 +0100 haftmann added predicate compiler, as formally checked prototype, not as user package
Sat, 28 Feb 2009 21:34:33 +0100 wenzelm A Serbian theory, by Filip Maric.
Thu, 05 Feb 2009 14:14:03 +0100 haftmann split of already properly working part of Quickcheck infrastructure
Tue, 03 Feb 2009 16:50:41 +0100 haftmann established session HOL-Reflection
Tue, 03 Feb 2009 07:44:10 +0100 haftmann repaired accidental commit
Sun, 01 Feb 2009 19:59:20 +0100 haftmann merged
Sun, 01 Feb 2009 19:59:04 +0100 haftmann added State_Monad theory in session
Fri, 30 Jan 2009 13:24:23 +0000 chaieb Added Formal_Power_Series_Examples to HOL-ex image
Wed, 28 Jan 2009 11:04:10 +0100 haftmann Reflection.thy now in HOL/Library
Tue, 06 Jan 2009 22:08:42 +0100 wenzelm more parallel loading;
Tue, 06 Jan 2009 21:55:51 +0100 wenzelm more parallel loading;
Sat, 27 Dec 2008 17:35:00 +0100 krauss renamed LexOrds.thy to Termination.thy; examples for sizechange method
Wed, 03 Dec 2008 15:58:44 +0100 haftmann made repository layout more coherent with logical distribution structure; stripped some $Id$s
Thu, 20 Nov 2008 19:43:34 +0100 wenzelm reactivated some dead theories (based on hints by Mark Hillebrand);
Thu, 16 Oct 2008 23:21:23 +0200 wenzelm removed Locales;
Thu, 25 Sep 2008 11:14:01 +0200 haftmann (temporary workaround)
Thu, 25 Sep 2008 10:17:23 +0200 haftmann (temporal deactivation)
Mon, 22 Sep 2008 22:59:35 +0200 berghofe Added examples for coherent logic prover.
Wed, 17 Sep 2008 21:27:14 +0200 wenzelm moved global ML bindings to global place;
Tue, 16 Sep 2008 16:13:06 +0200 haftmann moved term_of syntax to separate theory
Tue, 16 Sep 2008 09:21:24 +0200 haftmann evaluation using code generator
Wed, 03 Sep 2008 12:11:28 +0200 nipkow removed ex/Puzzle
Wed, 03 Sep 2008 00:11:27 +0200 kleing retired Ben Porter's DenumRat in favour of the shorter proof in
Tue, 02 Sep 2008 22:37:20 +0200 nipkow Replaced Library/NatPair by Nat_Int_Bij.
Wed, 27 Aug 2008 12:01:59 +0200 haftmann added HOL/ex/Numeral.thy
Tue, 05 Aug 2008 14:40:48 +0200 krauss fix HOL/ex/LexOrds.thy; add to regression
Fri, 25 Jul 2008 12:03:28 +0200 haftmann tuned
Thu, 03 Jul 2008 20:15:06 +0200 wenzelm removed old NSPrimes, cf. NSA/Examples/;
Wed, 02 Jul 2008 07:12:17 +0200 haftmann code antiquotation roaring ahead
Tue, 01 Jul 2008 07:58:17 +0200 haftmann HOL += HOL-Complex
Wed, 12 Mar 2008 19:38:14 +0100 haftmann separated Random.thy from Quickcheck.thy
Wed, 20 Feb 2008 23:24:38 +0100 wenzelm removed NBE;
Fri, 25 Jan 2008 23:05:27 +0100 wenzelm Codegenerator vs. Codegenerator_Pretty: loaded sequentially, due to hazardous ML sections;
Fri, 25 Jan 2008 14:53:56 +0100 haftmann distinguished examples for Efficient_Nat.thy
Thu, 20 Dec 2007 22:21:30 +0100 wenzelm included meson/metis tests in simultaneous use_thys;
Fri, 07 Dec 2007 10:59:03 +0100 krauss Adding "ex/Induction_Scheme.thy" to tests
Wed, 05 Dec 2007 14:16:15 +0100 haftmann dropped Classpackage.thy
Sat, 10 Nov 2007 14:36:33 +0100 wenzelm qualified Proofterm.proofs;
Fri, 12 Oct 2007 08:21:09 +0200 haftmann consolidated naming conventions for code generator theories
Thu, 11 Oct 2007 23:03:51 +0200 wenzelm enabled Refute_Examples again;
Thu, 11 Oct 2007 21:44:28 +0200 wenzelm disabled Refute_Examples temporarily;
Thu, 27 Sep 2007 17:22:15 +0200 wenzelm some more simultaneous use_thys;
Tue, 18 Sep 2007 05:42:46 +0200 nipkow Added function package to PreList
Thu, 06 Sep 2007 11:32:28 +0200 berghofe Integrated Executable_Rat and Executable_Real theories into
Wed, 05 Sep 2007 20:48:25 +0200 wenzelm tuned;
Wed, 29 Aug 2007 20:18:23 +0200 wenzelm some simultaneous use_thys;
Thu, 09 Aug 2007 15:52:45 +0200 haftmann tuned
Thu, 02 Aug 2007 15:44:37 +0200 wenzelm converted Meson tests to proper theory;
Thu, 19 Jul 2007 21:47:39 +0200 haftmann uniform naming conventions for CG theories
Mon, 16 Jul 2007 09:29:01 +0200 haftmann fixed SML/NJ int problem
Tue, 26 Jun 2007 13:01:48 +0200 nipkow added NBE
Thu, 21 Jun 2007 15:42:07 +0200 wenzelm replaced Real/Ferrante-Rackoff tool by generic version in Main HOL;
less more (0) -100 -60 tip