src/HOL/ex/ROOT.ML
Fri, 11 Mar 2011 10:37:41 +0100 bulwahn adding lazysmallcheck example theory to HOL-ex session
Sat, 15 Jan 2011 20:05:29 +0100 haftmann experimental variant of interpretation with simultaneous definitions, plus example
Fri, 07 Jan 2011 18:10:43 +0100 bulwahn adding example theory for list comprehension to set comprehension simproc
Wed, 29 Dec 2010 17:34:41 +0100 wenzelm explicit file specifications -- avoid secondary load path;
Fri, 03 Dec 2010 21:30:41 +0100 wenzelm eliminated fragile HTML.with_charset -- always use utf-8;
Mon, 22 Nov 2010 10:41:52 +0100 bulwahn adding birthday paradoxon from some abandoned drawer
Wed, 03 Nov 2010 12:20:33 +0100 haftmann moved theory Quicksort from Library/ to ex/
Fri, 29 Oct 2010 21:34:07 +0200 wenzelm Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
Thu, 28 Oct 2010 22:39:59 +0200 wenzelm moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref;
Wed, 15 Sep 2010 13:44:10 +0200 haftmann more explicit theory name
Mon, 06 Sep 2010 14:18:16 +0200 wenzelm more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
Mon, 06 Sep 2010 13:06:27 +0200 wenzelm some results of concurrency code inspection;
Wed, 21 Jul 2010 18:11:51 +0200 bulwahn added new theories to IsaMakefile and ROOT.ML
Fri, 09 Jul 2010 17:15:03 +0200 krauss moved example to its own file in HOL/ex
Fri, 02 Jul 2010 14:23:18 +0200 haftmann introduced distinct session HOL-Codegenerator_Test
Wed, 02 Jun 2010 13:18:21 +0200 wenzelm Hilbert_Classical: disable multithreading altogether, otherwise proof normalization will fork futures independently of Goal.parallel_proofs;
Mon, 17 May 2010 10:58:31 +0200 haftmann dropped old Library/Word.thy and toy example ex/Adder.thy
Mon, 10 May 2010 11:30:05 -0700 huffman put construction of reals using Dedekind cuts in HOL/ex
Wed, 24 Mar 2010 17:40:43 +0100 bulwahn moved further predicate compile files to HOL-Library
Wed, 24 Mar 2010 17:40:43 +0100 bulwahn moved examples for the predicate compiler into its own session Predicate_Compile_Examples to slenderise the HOL-ex session
Tue, 23 Feb 2010 17:33:03 +0100 hoelzl Moved old Integration to examples.
Wed, 17 Feb 2010 10:43:20 +0100 haftmann added simple theory about discrete summation
Wed, 17 Feb 2010 09:48:53 +0100 haftmann a draft for an example how to turn specifications involving choice executable
Thu, 12 Nov 2009 20:39:02 +0100 bulwahn adding the predicate compiler quickcheck to the ex/ROOT.ML; adopting this quickcheck to the latest changes
Tue, 10 Nov 2009 13:17:50 +0100 wenzelm try SAT_Examples last, to minimize impact of global side-effects;
Fri, 06 Nov 2009 14:42:42 +0100 krauss renamed method induct_scheme to induction_schema
Wed, 04 Nov 2009 16:54:22 +0100 nipkow New
Fri, 30 Oct 2009 13:59:49 +0100 haftmann moved Commutative_Ring into session Decision_Procs
Sun, 20 Sep 2009 18:15:07 +0200 wenzelm Hilbert_Classical: more precise control of parallel_proofs;
Fri, 11 Sep 2009 09:04:51 +0200 haftmann corrected upper/lowercase
Thu, 10 Sep 2009 15:23:08 +0200 haftmann split of test examples from NatTransfer
Tue, 01 Sep 2009 15:39:33 +0200 haftmann some reorganization of number theory
Fri, 28 Aug 2009 17:07:15 +0200 wenzelm SAT_Examples: removed obsolete Future.shutdown() workaround -- internal exception propagation should now work reliably;
Tue, 28 Jul 2009 19:49:42 +0200 wenzelm Future.shutdown before loading sequentially -- workaround scheduler deadlock;
Tue, 28 Jul 2009 18:17:35 +0200 wenzelm Hilbert_Classical: sequential loading due to @{prf}, which joins within a critical section (via options);
Tue, 28 Jul 2009 16:28:49 +0200 wenzelm non-critical use_thy;
Fri, 24 Jul 2009 11:31:22 +0200 wenzelm removed Formal_Power_Series_Examples (cf. adea7a729c7a);
Wed, 22 Jul 2009 10:45:35 +0200 wenzelm shutdown future scheduler after (failed) SAT_Examples, to workaround interference problem with follow-up theory loading;
Thu, 11 Jun 2009 19:49:02 +0200 haftmann merged
Tue, 09 Jun 2009 22:59:54 +0200 haftmann first running version of qc generators for datatypes
Thu, 11 Jun 2009 14:25:58 +0200 wenzelm merged, reverting workarounds on both sides;
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;
less more (0) -100 -60 tip