| 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
|
| Wed, 01 Dec 2010 11:01:20 +0100 |
wenzelm |
more precise dependencies;
|
file |
diff |
annotate
|
| Sat, 27 Nov 2010 17:44:36 -0800 |
huffman |
fix cut-and-paste errors for HOLCF entries in IsaMakefile
|
file |
diff |
annotate
|
| Sat, 27 Nov 2010 16:08:10 -0800 |
huffman |
moved directory src/HOLCF to src/HOL/HOLCF;
|
file |
diff |
annotate
|
| Tue, 23 Nov 2010 23:11:06 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 17:49:12 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 17:46:51 +0100 |
haftmann |
replaced misleading Fset/fset name -- these do not stand for finite sets
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 15:45:42 +0100 |
boehmes |
added prove reconstruction for injective functions;
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 11:34:56 +0100 |
bulwahn |
adding Enum to HOL-Main image and removing it from HOL-Library
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 10:41:54 +0100 |
bulwahn |
adding dependencies to IsaMakefile; adding sledgehammer_tactic in Mirabelle_Test
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 10:41:52 +0100 |
bulwahn |
adding birthday paradoxon from some abandoned drawer
|
file |
diff |
annotate
|
| Wed, 17 Nov 2010 11:09:18 +0100 |
haftmann |
module for functorial mappers
|
file |
diff |
annotate
|
| Mon, 08 Nov 2010 12:13:44 +0100 |
boehmes |
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
|
file |
diff |
annotate
|
| Mon, 08 Nov 2010 09:25:43 +0100 |
bulwahn |
adding code and theory for smallvalue generators, but do not setup the interpretation yet
|
file |
diff |
annotate
|
| Thu, 04 Nov 2010 13:37:11 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Wed, 03 Nov 2010 12:20:33 +0100 |
haftmann |
moved theory Quicksort from Library/ to ex/
|
file |
diff |
annotate
|
| Thu, 04 Nov 2010 09:53:23 +0100 |
blanchet |
moved file in makefile to reflect actual dependencies
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 21:34:07 +0200 |
wenzelm |
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 18:17:08 +0200 |
boehmes |
added crafted list of SMT built-in constants
|
file |
diff |
annotate
|
| Thu, 28 Oct 2010 22:39:59 +0200 |
wenzelm |
moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref;
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 12:17:19 +0200 |
blanchet |
reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 11:45:12 +0200 |
boehmes |
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
|
file |
diff |
annotate
|
| Mon, 25 Oct 2010 21:17:16 +0200 |
bulwahn |
adding new predicate compiler files to the IsaMakefile
|
file |
diff |
annotate
|
| Mon, 25 Oct 2010 13:36:20 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 25 Oct 2010 13:34:57 +0200 |
haftmann |
moved sledgehammer to Plain; tuned dependencies
|
file |
diff |
annotate
|
| Mon, 25 Oct 2010 11:42:05 +0200 |
blanchet |
merged
|
file |
diff |
annotate
|
| Mon, 25 Oct 2010 10:30:46 +0200 |
blanchet |
introduced manual version of "Auto Solve" as "solve_direct"
|
file |
diff |
annotate
|
| Sat, 23 Oct 2010 23:42:04 +0200 |
krauss |
integrated partial_function into HOL-Plain
|
file |
diff |
annotate
|
| Fri, 22 Oct 2010 18:38:59 +0200 |
bulwahn |
splitting Hotel Key card example into specification and the two tests for counter example generation
|
file |
diff |
annotate
|
| Fri, 22 Oct 2010 13:54:51 +0200 |
blanchet |
renamed files
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 11:10:37 +0200 |
blanchet |
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 10:28:11 +0200 |
blanchet |
factor out "Meson_Tactic" from "Meson_Clausify"
|
file |
diff |
annotate
|
| Mon, 04 Oct 2010 22:45:09 +0200 |
blanchet |
move Metis into Plain
|
file |
diff |
annotate
|
| Mon, 04 Oct 2010 22:01:34 +0200 |
blanchet |
added "Meson" theory to Makefile
|
file |
diff |
annotate
|
| Mon, 04 Oct 2010 21:37:42 +0200 |
blanchet |
move MESON files together
|
file |
diff |
annotate
|
| Wed, 29 Sep 2010 23:26:39 +0200 |
blanchet |
rename file
|
file |
diff |
annotate
|
| Wed, 29 Sep 2010 09:07:58 +0200 |
haftmann |
moved old_primrec source to nominal package, where it is still used
|
file |
diff |
annotate
|
| Tue, 28 Sep 2010 15:39:59 +0200 |
haftmann |
dropped old primrec package
|
file |
diff |
annotate
|
| Tue, 28 Sep 2010 12:47:55 +0200 |
haftmann |
modernized session
|
file |
diff |
annotate
|
| Mon, 27 Sep 2010 10:44:08 +0200 |
blanchet |
rename "Clausifier" to "Meson_Clausifier" and merge with "Meson_Tactic"
|
file |
diff |
annotate
|
| Thu, 23 Sep 2010 14:50:18 +0200 |
bulwahn |
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 15:10:21 +0200 |
haftmann |
Factored out ML into separate file
|
file |
diff |
annotate
|
| Fri, 17 Sep 2010 16:38:11 +0200 |
blanchet |
merged
|
file |
diff |
annotate
|
| Thu, 16 Sep 2010 16:24:23 +0200 |
blanchet |
added new "Metis_Reconstruct" module, temporarily empty
|
file |
diff |
annotate
|
| Thu, 16 Sep 2010 16:12:02 +0200 |
blanchet |
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
|
file |
diff |
annotate
|
| Fri, 17 Sep 2010 10:52:35 +0200 |
boehmes |
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
|
file |
diff |
annotate
|
| Thu, 16 Sep 2010 11:12:08 +0200 |
blanchet |
factored out TSTP/SPASS/Vampire proof parsing;
|
file |
diff |
annotate
|