| Tue, 28 Jul 2009 18:17:35 +0200 |
wenzelm |
Hilbert_Classical: sequential loading due to @{prf}, which joins within a critical section (via options);
|
file |
diff |
annotate
|
| Tue, 28 Jul 2009 16:28:49 +0200 |
wenzelm |
non-critical use_thy;
|
file |
diff |
annotate
|
| Fri, 24 Jul 2009 11:31:22 +0200 |
wenzelm |
removed Formal_Power_Series_Examples (cf. adea7a729c7a);
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Thu, 11 Jun 2009 19:49:02 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Tue, 09 Jun 2009 22:59:54 +0200 |
haftmann |
first running version of qc generators for datatypes
|
file |
diff |
annotate
|
| Thu, 11 Jun 2009 14:25:58 +0200 |
wenzelm |
merged, reverting workarounds on both sides;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Tue, 02 Jun 2009 18:26:01 +0200 |
haftmann |
added Landau theory
|
file |
diff |
annotate
|
| Tue, 02 Jun 2009 15:53:07 +0200 |
haftmann |
tuned code generator test theories
|
file |
diff |
annotate
|
| Fri, 15 May 2009 16:39:17 +0200 |
haftmann |
dropped theory Term_Of_Syntax
|
file |
diff |
annotate
|
| Tue, 12 May 2009 21:17:47 +0200 |
haftmann |
split Predicate_Compile examples into separate theory
|
file |
diff |
annotate
|
| Fri, 27 Mar 2009 10:05:13 +0100 |
haftmann |
dropped toy example Code_Antiq
|
file |
diff |
annotate
|
| Mon, 23 Mar 2009 19:01:17 +0100 |
haftmann |
moved Imperative_HOL examples to Imperative_HOL/ex
|
file |
diff |
annotate
|
| Wed, 11 Mar 2009 08:45:47 +0100 |
haftmann |
moved Decision_Procs examples to Decision_Procs/ex
|
file |
diff |
annotate
|
| Sun, 08 Mar 2009 15:25:28 +0100 |
haftmann |
added predicate compiler, as formally checked prototype, not as user package
|
file |
diff |
annotate
|
| Sat, 28 Feb 2009 21:34:33 +0100 |
wenzelm |
A Serbian theory, by Filip Maric.
|
file |
diff |
annotate
|
| Thu, 05 Feb 2009 14:14:03 +0100 |
haftmann |
split of already properly working part of Quickcheck infrastructure
|
file |
diff |
annotate
|
| Tue, 03 Feb 2009 16:50:41 +0100 |
haftmann |
established session HOL-Reflection
|
file |
diff |
annotate
|
| Tue, 03 Feb 2009 07:44:10 +0100 |
haftmann |
repaired accidental commit
|
file |
diff |
annotate
|
| Sun, 01 Feb 2009 19:59:20 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Sun, 01 Feb 2009 19:59:04 +0100 |
haftmann |
added State_Monad theory in session
|
file |
diff |
annotate
|
| Fri, 30 Jan 2009 13:24:23 +0000 |
chaieb |
Added Formal_Power_Series_Examples to HOL-ex image
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 11:04:10 +0100 |
haftmann |
Reflection.thy now in HOL/Library
|
file |
diff |
annotate
|
| Tue, 06 Jan 2009 22:08:42 +0100 |
wenzelm |
more parallel loading;
|
file |
diff |
annotate
|
| Tue, 06 Jan 2009 21:55:51 +0100 |
wenzelm |
more parallel loading;
|
file |
diff |
annotate
|
| Sat, 27 Dec 2008 17:35:00 +0100 |
krauss |
renamed LexOrds.thy to Termination.thy; examples for sizechange method
|
file |
diff |
annotate
|
| Wed, 03 Dec 2008 15:58:44 +0100 |
haftmann |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
|
file |
diff |
annotate
|
| Thu, 20 Nov 2008 19:43:34 +0100 |
wenzelm |
reactivated some dead theories (based on hints by Mark Hillebrand);
|
file |
diff |
annotate
|
| Thu, 16 Oct 2008 23:21:23 +0200 |
wenzelm |
removed Locales;
|
file |
diff |
annotate
|
| Thu, 25 Sep 2008 11:14:01 +0200 |
haftmann |
(temporary workaround)
|
file |
diff |
annotate
|
| Thu, 25 Sep 2008 10:17:23 +0200 |
haftmann |
(temporal deactivation)
|
file |
diff |
annotate
|
| Mon, 22 Sep 2008 22:59:35 +0200 |
berghofe |
Added examples for coherent logic prover.
|
file |
diff |
annotate
|
| Wed, 17 Sep 2008 21:27:14 +0200 |
wenzelm |
moved global ML bindings to global place;
|
file |
diff |
annotate
|
| Tue, 16 Sep 2008 16:13:06 +0200 |
haftmann |
moved term_of syntax to separate theory
|
file |
diff |
annotate
|
| Tue, 16 Sep 2008 09:21:24 +0200 |
haftmann |
evaluation using code generator
|
file |
diff |
annotate
|
| Wed, 03 Sep 2008 12:11:28 +0200 |
nipkow |
removed ex/Puzzle
|
file |
diff |
annotate
|
| Wed, 03 Sep 2008 00:11:27 +0200 |
kleing |
retired Ben Porter's DenumRat in favour of the shorter proof in
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 22:37:20 +0200 |
nipkow |
Replaced Library/NatPair by Nat_Int_Bij.
|
file |
diff |
annotate
|
| Wed, 27 Aug 2008 12:01:59 +0200 |
haftmann |
added HOL/ex/Numeral.thy
|
file |
diff |
annotate
|
| Tue, 05 Aug 2008 14:40:48 +0200 |
krauss |
fix HOL/ex/LexOrds.thy; add to regression
|
file |
diff |
annotate
|
| Fri, 25 Jul 2008 12:03:28 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Thu, 03 Jul 2008 20:15:06 +0200 |
wenzelm |
removed old NSPrimes, cf. NSA/Examples/;
|
file |
diff |
annotate
|
| Wed, 02 Jul 2008 07:12:17 +0200 |
haftmann |
code antiquotation roaring ahead
|
file |
diff |
annotate
|
| Tue, 01 Jul 2008 07:58:17 +0200 |
haftmann |
HOL += HOL-Complex
|
file |
diff |
annotate
|
| Wed, 12 Mar 2008 19:38:14 +0100 |
haftmann |
separated Random.thy from Quickcheck.thy
|
file |
diff |
annotate
|
| Wed, 20 Feb 2008 23:24:38 +0100 |
wenzelm |
removed NBE;
|
file |
diff |
annotate
|
| Fri, 25 Jan 2008 23:05:27 +0100 |
wenzelm |
Codegenerator vs. Codegenerator_Pretty: loaded sequentially, due to hazardous ML sections;
|
file |
diff |
annotate
|
| Fri, 25 Jan 2008 14:53:56 +0100 |
haftmann |
distinguished examples for Efficient_Nat.thy
|
file |
diff |
annotate
|
| Thu, 20 Dec 2007 22:21:30 +0100 |
wenzelm |
included meson/metis tests in simultaneous use_thys;
|
file |
diff |
annotate
|
| Fri, 07 Dec 2007 10:59:03 +0100 |
krauss |
Adding "ex/Induction_Scheme.thy" to tests
|
file |
diff |
annotate
|
| Wed, 05 Dec 2007 14:16:15 +0100 |
haftmann |
dropped Classpackage.thy
|
file |
diff |
annotate
|
| Sat, 10 Nov 2007 14:36:33 +0100 |
wenzelm |
qualified Proofterm.proofs;
|
file |
diff |
annotate
|
| Fri, 12 Oct 2007 08:21:09 +0200 |
haftmann |
consolidated naming conventions for code generator theories
|
file |
diff |
annotate
|
| Thu, 11 Oct 2007 23:03:51 +0200 |
wenzelm |
enabled Refute_Examples again;
|
file |
diff |
annotate
|
| Thu, 11 Oct 2007 21:44:28 +0200 |
wenzelm |
disabled Refute_Examples temporarily;
|
file |
diff |
annotate
|
| Thu, 27 Sep 2007 17:22:15 +0200 |
wenzelm |
some more simultaneous use_thys;
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 05:42:46 +0200 |
nipkow |
Added function package to PreList
|
file |
diff |
annotate
|
| Thu, 06 Sep 2007 11:32:28 +0200 |
berghofe |
Integrated Executable_Rat and Executable_Real theories into
|
file |
diff |
annotate
|
| Wed, 05 Sep 2007 20:48:25 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|