Fri, 16 Dec 2011 10:52:35 +0100 |
wenzelm |
clarified modules that contribute to datatype package;
|
file |
diff |
annotate
|
Thu, 15 Dec 2011 17:37:14 +0100 |
wenzelm |
separate rep_datatype.ML;
|
file |
diff |
annotate
|
Thu, 15 Dec 2011 09:13:32 +0100 |
nipkow |
merged
|
file |
diff |
annotate
|
Thu, 15 Dec 2011 09:13:23 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
Wed, 14 Dec 2011 18:07:32 +0100 |
blanchet |
added new proof redirection code
|
file |
diff |
annotate
|
Wed, 14 Dec 2011 16:30:32 +0100 |
bulwahn |
correcting dependencies after renaming
|
file |
diff |
annotate
|
Wed, 14 Dec 2011 12:02:02 +0100 |
wenzelm |
more visible benchmarks;
|
file |
diff |
annotate
|
Sun, 11 Dec 2011 18:22:06 +0100 |
nipkow |
added IMP/Live_True.thy
|
file |
diff |
annotate
|
Fri, 09 Dec 2011 14:46:18 +0100 |
kuncar |
added dependencies
|
file |
diff |
annotate
|
Sun, 04 Dec 2011 18:30:57 +0100 |
huffman |
merged
|
file |
diff |
annotate
|
Sun, 04 Dec 2011 13:10:19 +0100 |
huffman |
remove Library/Diagonalize.thy, because Library/Nat_Bijection.thy includes all the same functionality
|
file |
diff |
annotate
|
Sun, 04 Dec 2011 18:29:29 +0100 |
nipkow |
missing dependency
|
file |
diff |
annotate
|
Thu, 01 Dec 2011 20:52:16 +0100 |
nipkow |
merged IMP/Util into IMP/Vars
|
file |
diff |
annotate
|
Tue, 29 Nov 2011 22:45:21 +0100 |
wenzelm |
more conventional file name;
|
file |
diff |
annotate
|
Fri, 18 Nov 2011 13:50:01 +0100 |
bulwahn |
adding another example for lifting definitions
|
file |
diff |
annotate
|
Thu, 17 Nov 2011 19:01:05 +0100 |
bulwahn |
adding a preliminary example to show how the quotient_definition package can be generalized
|
file |
diff |
annotate
|
Mon, 14 Nov 2011 11:50:52 +0100 |
hoelzl |
add Code_Real_Approx_By_Float
|
file |
diff |
annotate
|
Sun, 06 Nov 2011 16:22:26 +0100 |
wenzelm |
more precise dependencies;
|
file |
diff |
annotate
|
Thu, 03 Nov 2011 10:29:05 +1100 |
kleing |
moved latex generation for HOL-IMP out of distribution
|
file |
diff |
annotate
|
Tue, 01 Nov 2011 10:05:28 +0100 |
bulwahn |
renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)
|
file |
diff |
annotate
|
Tue, 25 Oct 2011 16:37:11 +0200 |
bulwahn |
renaming Cset and List_Cset in Quotient_Examples to Quotient_Set and List_Quotient_Set to avoid a name clash of theory names with the ones in HOL-Library
|
file |
diff |
annotate
|
Mon, 24 Oct 2011 10:45:54 +0200 |
nipkow |
latex output not needed because errors manifest themselves earlier
|
file |
diff |
annotate
|
Sat, 22 Oct 2011 20:17:50 +0200 |
nipkow |
added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
|
file |
diff |
annotate
|
Fri, 21 Oct 2011 08:42:11 +0200 |
huffman |
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
|
file |
diff |
annotate
|
Wed, 19 Oct 2011 09:11:20 +0200 |
bulwahn |
removing old code generator
|
file |
diff |
annotate
|
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
|
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
|