| Tue, 20 Sep 2011 05:47:11 +0200 |
nipkow |
New proof method "induction" that gives induction hypotheses the name IH.
|
file |
diff |
annotate
|
| Sun, 18 Sep 2011 13:39:33 +0200 |
wenzelm |
finite sequences as useful as introductory example;
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 09:28:03 +0200 |
bulwahn |
correcting theory name and dependencies
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 10:57:58 +0200 |
bulwahn |
moving connection of association lists to Mappings into a separate theory
|
file |
diff |
annotate
|
| Sat, 10 Sep 2011 10:29:24 +0200 |
haftmann |
renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 23:38:52 +0200 |
haftmann |
theory of saturated naturals contributed by Peter Gammie
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 19:25:44 +0200 |
nipkow |
merged
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 19:25:18 +0200 |
nipkow |
Added Abstract Interpretation theories
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 14:43:20 +0200 |
blanchet |
renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
|
file |
diff |
annotate
|
| Wed, 24 Aug 2011 15:06:13 -0700 |
huffman |
move everything related to 'norm' method into new theory file Norm_Arith.thy
|
file |
diff |
annotate
|
| Sun, 21 Aug 2011 22:13:04 +0200 |
krauss |
removed session HOL/Subst -- now subsumed my more modern HOL/ex/Unification.thy
|
file |
diff |
annotate
|
| Thu, 18 Aug 2011 18:10:23 -0700 |
huffman |
add Multivariate_Analysis dependencies
|
file |
diff |
annotate
|
| Thu, 18 Aug 2011 13:10:24 +0200 |
haftmann |
avoid case-sensitive name for example theory
|
file |
diff |
annotate
|
| Wed, 17 Aug 2011 14:32:48 -0700 |
huffman |
IsaMakefile: target HOLCF-Library now compiles HOL/HOLCF/Library instead of HOL/Library
|
file |
diff |
annotate
|
| Wed, 17 Aug 2011 13:14:20 +0200 |
wenzelm |
moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
|
file |
diff |
annotate
|
| Thu, 11 Aug 2011 09:41:21 +0200 |
krauss |
removed obsolete recdef-related examples
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 20:12:36 +0200 |
wenzelm |
moved old code generator to src/Tools/;
|
file |
diff |
annotate
|
| Tue, 09 Aug 2011 09:05:21 +0200 |
blanchet |
load lambda-lifting structure earlier, so it can be used in Metis
|
file |
diff |
annotate
|
| Tue, 02 Aug 2011 11:52:57 +0200 |
krauss |
moved recursion combinator to HOL/Library/Wfrec.thy -- it is so fundamental and well-known that it should survive recdef
|
file |
diff |
annotate
|
| Tue, 02 Aug 2011 10:36:50 +0200 |
krauss |
moved recdef package to HOL/Library/Old_Recdef.thy
|
file |
diff |
annotate
|
| Mon, 01 Aug 2011 09:31:10 -0700 |
huffman |
new theory HOL/Library/Product_Lattice.thy
|
file |
diff |
annotate
|
| Tue, 26 Jul 2011 18:11:38 +0200 |
bulwahn |
more precise dependencies
|
file |
diff |
annotate
|
| Mon, 25 Jul 2011 10:43:14 +0200 |
bulwahn |
removing SML_Quickcheck
|
file |
diff |
annotate
|
| Wed, 20 Jul 2011 13:29:54 +0200 |
boehmes |
more precise dependencies
|
file |
diff |
annotate
|
| Wed, 20 Jul 2011 13:27:01 +0200 |
boehmes |
merged
|
file |
diff |
annotate
|
| Wed, 20 Jul 2011 09:23:09 +0200 |
boehmes |
removed old (unused) SMT monomorphizer
|
file |
diff |
annotate
|
| Wed, 20 Jul 2011 10:48:00 +0200 |
hoelzl |
merged
|
file |
diff |
annotate
|
| Tue, 19 Jul 2011 14:36:12 +0200 |
hoelzl |
Rename extreal => ereal
|
file |
diff |
annotate
|
| Tue, 19 Jul 2011 14:35:44 +0200 |
hoelzl |
rename Nat_Infinity (inat) to Extended_Nat (enat)
|
file |
diff |
annotate
|
| Wed, 20 Jul 2011 10:11:08 +0200 |
Cezary Kaliszyk |
HOL/Import reorganization/cleaning. Factor 9 speedup. Remove Import XML parser in favor of much faster of Isabelle's XML parser. Remove ImportRecording since we can use Isabelle images.
|
file |
diff |
annotate
|
| Wed, 20 Jul 2011 08:46:17 +0200 |
kleing |
build an image for HOL-IMP
|
file |
diff |
annotate
|
| Thu, 14 Jul 2011 22:08:11 +0200 |
krauss |
added missing dependencies;
|
file |
diff |
annotate
|
| Wed, 13 Jul 2011 22:16:19 +0200 |
blanchet |
cleanly separate TPTP related files from other examples
|
file |
diff |
annotate
|
| Wed, 13 Jul 2011 15:50:45 +0200 |
krauss |
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
|
file |
diff |
annotate
|
| Wed, 06 Jul 2011 17:19:34 +0100 |
blanchet |
moved ATP dependencies to HOL-Plain, where they belong
|
file |
diff |
annotate
|
| Fri, 01 Jul 2011 11:26:02 +0200 |
bulwahn |
improving actual dependencies
|
file |
diff |
annotate
|
| Mon, 27 Jun 2011 09:42:46 +0200 |
hoelzl |
move conditional expectation to its own theory file
|
file |
diff |
annotate
|
| 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
|