| Wed, 19 Oct 2011 08:37:25 +0200 |
bulwahn |
removing old code generator for inductive predicates
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 08:37:16 +0200 |
bulwahn |
removing old code generator setup in the HOL theory
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 08:37:15 +0200 |
bulwahn |
removing invocations of the evaluation method based on the old code generator
|
file |
diff |
annotate
|
| Wed, 28 Sep 2011 09:59:55 +0200 |
nipkow |
Added dependecies
|
file |
diff |
annotate
|
| Wed, 28 Sep 2011 09:55:11 +0200 |
nipkow |
Added Hoare-like Abstract Interpretation
|
file |
diff |
annotate
|
| Wed, 28 Sep 2011 08:51:55 +0200 |
nipkow |
moved IMP/AbsInt stuff into subdirectory Abs_Int_Den
|
file |
diff |
annotate
|
| Mon, 26 Sep 2011 20:39:18 +0200 |
wenzelm |
reverted 09cdc4209d25 for formal reasons: it did not say what was "broken" nor "fixed", but broke IsaMakefile dependencies;
|
file |
diff |
annotate
|
| Sun, 25 Sep 2011 09:37:33 +0200 |
haftmann |
Quotient_Set.thy is part of library
|
file |
diff |
annotate
|
| Sat, 24 Sep 2011 00:17:32 +0100 |
sultana |
fixed IsaMakefile action for HOL-TPTP.
|
file |
diff |
annotate
|
| Thu, 22 Sep 2011 18:23:38 +0200 |
berghofe |
Moved extraction part of Higman's lemma to separate theory to allow reuse in
|
file |
diff |
annotate
|
| Thu, 22 Sep 2011 16:50:23 +0200 |
berghofe |
Added documentation for HOL-SPARK
|
file |
diff |
annotate
|
| Wed, 21 Sep 2011 15:55:16 +0200 |
blanchet |
reintroduced Minipick as Nitpick example
|
file |
diff |
annotate
|
| Wed, 21 Sep 2011 07:03:16 +0200 |
nipkow |
added missing makefile dependence
|
file |
diff |
annotate
|
| 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
|