| 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;
|
file |
diff |
annotate
|
| Mon, 17 May 2010 10:58:31 +0200 |
haftmann |
dropped old Library/Word.thy and toy example ex/Adder.thy
|
file |
diff |
annotate
|
| Mon, 10 May 2010 11:30:05 -0700 |
huffman |
put construction of reals using Dedekind cuts in HOL/ex
|
file |
diff |
annotate
|
| Wed, 24 Mar 2010 17:40:43 +0100 |
bulwahn |
moved further predicate compile files to HOL-Library
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Tue, 23 Feb 2010 17:33:03 +0100 |
hoelzl |
Moved old Integration to examples.
|
file |
diff |
annotate
|
| Wed, 17 Feb 2010 10:43:20 +0100 |
haftmann |
added simple theory about discrete summation
|
file |
diff |
annotate
|
| Wed, 17 Feb 2010 09:48:53 +0100 |
haftmann |
a draft for an example how to turn specifications involving choice executable
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Tue, 10 Nov 2009 13:17:50 +0100 |
wenzelm |
try SAT_Examples last, to minimize impact of global side-effects;
|
file |
diff |
annotate
|
| Fri, 06 Nov 2009 14:42:42 +0100 |
krauss |
renamed method induct_scheme to induction_schema
|
file |
diff |
annotate
|
| Wed, 04 Nov 2009 16:54:22 +0100 |
nipkow |
New
|
file |
diff |
annotate
|
| Fri, 30 Oct 2009 13:59:49 +0100 |
haftmann |
moved Commutative_Ring into session Decision_Procs
|
file |
diff |
annotate
|
| Sun, 20 Sep 2009 18:15:07 +0200 |
wenzelm |
Hilbert_Classical: more precise control of parallel_proofs;
|
file |
diff |
annotate
|
| Fri, 11 Sep 2009 09:04:51 +0200 |
haftmann |
corrected upper/lowercase
|
file |
diff |
annotate
|
| Thu, 10 Sep 2009 15:23:08 +0200 |
haftmann |
split of test examples from NatTransfer
|
file |
diff |
annotate
|
| Tue, 01 Sep 2009 15:39:33 +0200 |
haftmann |
some reorganization of number theory
|
file |
diff |
annotate
|
| Fri, 28 Aug 2009 17:07:15 +0200 |
wenzelm |
SAT_Examples: removed obsolete Future.shutdown() workaround -- internal exception propagation should now work reliably;
|
file |
diff |
annotate
|
| Tue, 28 Jul 2009 19:49:42 +0200 |
wenzelm |
Future.shutdown before loading sequentially -- workaround scheduler deadlock;
|
file |
diff |
annotate
|
| 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
|