| 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
|
| 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
|
| Mon, 03 Jan 2011 16:22:08 +0100 |
boehmes |
re-implemented support for datatypes (including records and typedefs);
|
file |
diff |
annotate
|
| Wed, 29 Dec 2010 17:34:41 +0100 |
wenzelm |
explicit file specifications -- avoid secondary load path;
|
file |
diff |
annotate
|
| Wed, 29 Dec 2010 12:16:49 +0100 |
wenzelm |
made SML/NJ happy;
|
file |
diff |
annotate
|
| Tue, 21 Dec 2010 10:24:56 +0100 |
blanchet |
renamed "sledgehammer_tactic.ML" to "sledgehammer_tactics.ML" (cf. module name);
|
file |
diff |
annotate
|
| Sun, 19 Dec 2010 05:15:31 -0800 |
huffman |
reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
|
file |
diff |
annotate
|
| Sun, 19 Dec 2010 04:06:02 -0800 |
huffman |
renamed Bifinite.thy to Representable.thy
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 16:43:45 -0800 |
huffman |
renamed CompactBasis.thy to Compact_Basis.thy
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 11:26:28 +0100 |
blanchet |
example tuning
|
file |
diff |
annotate
|
| Sat, 11 Dec 2010 21:27:53 -0800 |
huffman |
add HOLCF library theories with cpo/predomain instances for HOL types
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 22:17:52 +0100 |
blanchet |
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 15:55:35 +0100 |
boehmes |
merged
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 14:53:44 +0100 |
boehmes |
moved smt_word.ML into the directory of the Word library
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 09:58:56 +0100 |
blanchet |
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 15:25:14 +0100 |
hoelzl |
it is known as the extended reals, not the infinite reals
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 09:25:05 +0100 |
haftmann |
moved bootstrap of type_lifting to Fun
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 09:19:10 +0100 |
haftmann |
replace `type_mapper` by the more adequate `type_lifting`
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 17:59:13 +0100 |
wenzelm |
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
|
file |
diff |
annotate
|
| Wed, 01 Dec 2010 19:42:09 +0100 |
hoelzl |
Corrected IsaMakefile
|
file |
diff |
annotate
|
| Wed, 01 Dec 2010 19:36:05 +0100 |
hoelzl |
merged
|
file |
diff |
annotate
|
| Wed, 01 Dec 2010 19:27:53 +0100 |
hoelzl |
More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability.
|
file |
diff |
annotate
|
| Wed, 01 Dec 2010 18:00:40 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Wed, 01 Dec 2010 11:33:17 +0100 |
haftmann |
file for package tool type_mapper carries the same name as its Isar command
|
file |
diff |
annotate
|
| Wed, 01 Dec 2010 11:32:24 +0100 |
wenzelm |
activate subtyping/coercions in theory Complex_Main;
|
file |
diff |
annotate
|