| Wed, 22 Jun 2011 13:30:28 -0700 |
huffman |
add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
|
file |
diff |
annotate
|
| Fri, 17 Jun 2011 20:38:43 +0200 |
kleing |
IMP compiler with int, added reverse soundness direction
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 08:32:15 +0200 |
bulwahn |
adapting IsaMakefile
|
file |
diff |
annotate
|
| Tue, 07 Jun 2011 11:24:16 +0200 |
bulwahn |
merged; manually merged IsaMakefile
|
file |
diff |
annotate
|
| Tue, 07 Jun 2011 11:12:05 +0200 |
bulwahn |
splitting Cset into Cset and List_Cset
|
file |
diff |
annotate
|
| Tue, 07 Jun 2011 11:10:57 +0200 |
bulwahn |
renaming the formalisation of the birthday problem to a proper English name
|
file |
diff |
annotate
|
| Tue, 07 Jun 2011 07:04:53 +0200 |
blanchet |
renamed example theory to "ATP_Export", for consistency with its underlying "ATP_" modules
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
tuned Metis examples
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:34 +0200 |
blanchet |
added Metis examples to test the new type encodings
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 16:29:38 +0200 |
kleing |
imported rest of new IMP
|
file |
diff |
annotate
|
| Thu, 02 Jun 2011 10:10:23 +0200 |
nipkow |
Added typed IMP
|
file |
diff |
annotate
|
| Thu, 02 Jun 2011 08:55:08 +0200 |
bulwahn |
splitting Dlist theory in Dlist and Dlist_Cset
|
file |
diff |
annotate
|
| Wed, 01 Jun 2011 21:50:49 +0200 |
nipkow |
Removed old IMP files
|
file |
diff |
annotate
|
| Wed, 01 Jun 2011 09:10:13 +0200 |
bulwahn |
splitting RBT theory into RBT and RBT_Mapping
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
use "monomorph.ML" in "ATP" theory (so the new Metis can use it)
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
first step in sharing more code between ATP and Metis translation
|
file |
diff |
annotate
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
renamed "Auto_Tools" "Try"
|
file |
diff |
annotate
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
renamed "try" "try_methods"
|
file |
diff |
annotate
|
| Tue, 17 May 2011 11:47:36 +0200 |
hoelzl |
Add formalization of probabilistic independence for families of sets
|
file |
diff |
annotate
|
| Wed, 18 May 2011 15:45:33 +0200 |
bulwahn |
adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages
|
file |
diff |
annotate
|
| Mon, 02 May 2011 12:09:33 +0200 |
blanchet |
added TPTP exporter facility -- useful to do experiments with machine learning
|
file |
diff |
annotate
|
| Mon, 02 May 2011 12:09:33 +0200 |
blanchet |
renamed theory to make its purpose clearer
|
file |
diff |
annotate
|
| Thu, 14 Apr 2011 11:24:05 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
| Thu, 14 Apr 2011 11:24:04 +0200 |
blanchet |
started clausifier examples
|
file |
diff |
annotate
|
| Wed, 30 Mar 2011 10:31:02 +0200 |
bulwahn |
adding a regression test for SML_Quickcheck; putting SML_Quickcheck back in shape
|
file |
diff |
annotate
|
| Tue, 29 Mar 2011 21:48:01 +0200 |
wenzelm |
use shared copy of hoare_syntax.ML;
|
file |
diff |
annotate
|
| Tue, 29 Mar 2011 14:27:42 +0200 |
hoelzl |
rename Probability_Space to Probability_Measure
|
file |
diff |
annotate
|
| Tue, 29 Mar 2011 14:27:41 +0200 |
hoelzl |
add infinite product measure
|
file |
diff |
annotate
|
| Tue, 29 Mar 2011 14:27:39 +0200 |
hoelzl |
split Product_Measure into Binary_Product_Measure and Finite_Product_Measure
|
file |
diff |
annotate
|
| Sun, 27 Mar 2011 17:32:25 +0200 |
krauss |
added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj";
|
file |
diff |
annotate
|
| Wed, 23 Mar 2011 10:06:27 +0100 |
blanchet |
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
|
file |
diff |
annotate
|
| Tue, 22 Mar 2011 19:04:32 +0100 |
blanchet |
added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter
|
file |
diff |
annotate
|
| Tue, 22 Mar 2011 18:38:29 +0100 |
blanchet |
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
|
file |
diff |
annotate
|
| Mon, 21 Mar 2011 14:25:59 +0100 |
krauss |
more precise dependencies
|
file |
diff |
annotate
|
| Mon, 21 Mar 2011 12:43:26 +0100 |
krauss |
small test case for main mirabelle functionality, which easily breaks without noticing
|
file |
diff |
annotate
|
| Mon, 14 Mar 2011 14:37:49 +0100 |
hoelzl |
reworked Probability theory: measures are not type restricted to positive extended reals
|
file |
diff |
annotate
|
| Mon, 14 Mar 2011 14:37:47 +0100 |
hoelzl |
split Extended_Reals into parts for Library and Multivariate_Analysis
|
file |
diff |
annotate
|
| Mon, 14 Mar 2011 14:37:39 +0100 |
hoelzl |
add Extended_Reals from AFP/Lower_Semicontinuous
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 23:12:38 +0100 |
wenzelm |
eliminated Bali.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 9b19cbb0af28;
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 15:21:13 +0100 |
bulwahn |
adaptions in generators using the common functions
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 15:21:13 +0100 |
bulwahn |
adding file quickcheck_common to carry common functions of all quickcheck generators
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 15:21:13 +0100 |
bulwahn |
correcting dependencies in IsaMakefile
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 15:21:13 +0100 |
bulwahn |
moving exhaustive_generators.ML to Quickcheck directory
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 15:21:13 +0100 |
bulwahn |
correcting dependencies after renaming
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 10:37:41 +0100 |
bulwahn |
adding lazysmallcheck example theory to HOL-ex session
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 10:37:36 +0100 |
bulwahn |
adding Lazysmallcheck prototype to HOL-Library
|
file |
diff |
annotate
|
| Thu, 03 Mar 2011 22:06:15 +0100 |
wenzelm |
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;
|
file |
diff |
annotate
|
| Sat, 26 Feb 2011 20:16:44 +0100 |
nipkow |
Corrected HOLCF/FOCUS dependency
|
file |
diff |
annotate
|
| Sat, 26 Feb 2011 16:16:36 +0100 |
nipkow |
corrected HOLCF dependency on Nat_Infinity
|
file |
diff |
annotate
|
| Wed, 23 Feb 2011 11:23:26 +0100 |
noschinl |
setup case_product attribute in HOL and FOL
|
file |
diff |
annotate
|
| Wed, 19 Jan 2011 11:34:10 +0100 |
hoelzl |
merged
|
file |
diff |
annotate
|
| Tue, 18 Jan 2011 21:37:23 +0100 |
hoelzl |
Gauge measure removed
|
file |
diff |
annotate
|
| Sat, 15 Jan 2011 20:05:29 +0100 |
haftmann |
experimental variant of interpretation with simultaneous definitions, plus example
|
file |
diff |
annotate
|
| Sat, 15 Jan 2011 13:41:58 +0100 |
berghofe |
Also added SPARK to test and clean targets.
|
file |
diff |
annotate
|
| Sat, 15 Jan 2011 12:48:39 +0100 |
berghofe |
Added HOL-SPARK and removed old_primrec.ML
|
file |
diff |
annotate
|
| Tue, 11 Jan 2011 14:12:37 +0100 |
haftmann |
"enriched_type" replaces less specific "type_lifting"
|
file |
diff |
annotate
|
| Mon, 10 Jan 2011 17:37:11 +0100 |
krauss |
removed obsolete make target (now in doc-src, cf. 28b487cd9e15)
|
file |
diff |
annotate
|
| Sat, 08 Jan 2011 17:39:51 +0100 |
wenzelm |
renamed Sum_Of_Squares to Sum_of_Squares;
|
file |
diff |
annotate
|
| Fri, 07 Jan 2011 18:10:43 +0100 |
bulwahn |
adding example theory for list comprehension to set comprehension simproc
|
file |
diff |
annotate
|
| Fri, 07 Jan 2011 18:10:35 +0100 |
bulwahn |
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
|
file |
diff |
annotate
|