| Tue, 29 Mar 2011 14:27:39 +0200 |
split Product_Measure into Binary_Product_Measure and Finite_Product_Measure
|
file | diff | annotate |
| Sun, 27 Mar 2011 17:32:25 +0200 |
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 |
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
|
file | diff | annotate |
| Tue, 22 Mar 2011 19:04:32 +0100 |
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 |
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 |
more precise dependencies
|
file | diff | annotate |
| Mon, 21 Mar 2011 12:43:26 +0100 |
small test case for main mirabelle functionality, which easily breaks without noticing
|
file | diff | annotate |
| Mon, 14 Mar 2011 14:37:49 +0100 |
reworked Probability theory: measures are not type restricted to positive extended reals
|
file | diff | annotate |
| Mon, 14 Mar 2011 14:37:47 +0100 |
split Extended_Reals into parts for Library and Multivariate_Analysis
|
file | diff | annotate |
| Mon, 14 Mar 2011 14:37:39 +0100 |
add Extended_Reals from AFP/Lower_Semicontinuous
|
file | diff | annotate |
| Sun, 13 Mar 2011 23:12:38 +0100 |
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 |
adaptions in generators using the common functions
|
file | diff | annotate |
| Fri, 11 Mar 2011 15:21:13 +0100 |
adding file quickcheck_common to carry common functions of all quickcheck generators
|
file | diff | annotate |
| Fri, 11 Mar 2011 15:21:13 +0100 |
correcting dependencies in IsaMakefile
|
file | diff | annotate |
| Fri, 11 Mar 2011 15:21:13 +0100 |
moving exhaustive_generators.ML to Quickcheck directory
|
file | diff | annotate |
| Fri, 11 Mar 2011 15:21:13 +0100 |
correcting dependencies after renaming
|
file | diff | annotate |
| Fri, 11 Mar 2011 10:37:41 +0100 |
adding lazysmallcheck example theory to HOL-ex session
|
file | diff | annotate |
| Fri, 11 Mar 2011 10:37:36 +0100 |
adding Lazysmallcheck prototype to HOL-Library
|
file | diff | annotate |
| Thu, 03 Mar 2011 22:06:15 +0100 |
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 |
Corrected HOLCF/FOCUS dependency
|
file | diff | annotate |
| Sat, 26 Feb 2011 16:16:36 +0100 |
corrected HOLCF dependency on Nat_Infinity
|
file | diff | annotate |
| Wed, 23 Feb 2011 11:23:26 +0100 |
setup case_product attribute in HOL and FOL
|
file | diff | annotate |
| Wed, 19 Jan 2011 11:34:10 +0100 |
merged
|
file | diff | annotate |
| Tue, 18 Jan 2011 21:37:23 +0100 |
Gauge measure removed
|
file | diff | annotate |
| Sat, 15 Jan 2011 20:05:29 +0100 |
experimental variant of interpretation with simultaneous definitions, plus example
|
file | diff | annotate |
| Sat, 15 Jan 2011 13:41:58 +0100 |
Also added SPARK to test and clean targets.
|
file | diff | annotate |
| Sat, 15 Jan 2011 12:48:39 +0100 |
Added HOL-SPARK and removed old_primrec.ML
|
file | diff | annotate |
| Tue, 11 Jan 2011 14:12:37 +0100 |
"enriched_type" replaces less specific "type_lifting"
|
file | diff | annotate |
| Mon, 10 Jan 2011 17:37:11 +0100 |
removed obsolete make target (now in doc-src, cf. 28b487cd9e15)
|
file | diff | annotate |
| Sat, 08 Jan 2011 17:39:51 +0100 |
renamed Sum_Of_Squares to Sum_of_Squares;
|
file | diff | annotate |
| Fri, 07 Jan 2011 18:10:43 +0100 |
adding example theory for list comprehension to set comprehension simproc
|
file | diff | annotate |
| Fri, 07 Jan 2011 18:10:35 +0100 |
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
|
file | diff | annotate |
| Mon, 03 Jan 2011 16:22:08 +0100 |
re-implemented support for datatypes (including records and typedefs);
|
file | diff | annotate |
| Wed, 29 Dec 2010 17:34:41 +0100 |
explicit file specifications -- avoid secondary load path;
|
file | diff | annotate |
| Wed, 29 Dec 2010 12:16:49 +0100 |
made SML/NJ happy;
|
file | diff | annotate |
| Tue, 21 Dec 2010 10:24:56 +0100 |
renamed "sledgehammer_tactic.ML" to "sledgehammer_tactics.ML" (cf. module name);
|
file | diff | annotate |
| Sun, 19 Dec 2010 05:15:31 -0800 |
reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
|
file | diff | annotate |
| Sun, 19 Dec 2010 04:06:02 -0800 |
renamed Bifinite.thy to Representable.thy
|
file | diff | annotate |
| Fri, 17 Dec 2010 16:43:45 -0800 |
renamed CompactBasis.thy to Compact_Basis.thy
|
file | diff | annotate |
| Wed, 15 Dec 2010 11:26:28 +0100 |
example tuning
|
file | diff | annotate |
| Sat, 11 Dec 2010 21:27:53 -0800 |
add HOLCF library theories with cpo/predomain instances for HOL types
|
file | diff | annotate |
| Wed, 08 Dec 2010 22:17:52 +0100 |
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
|
file | diff | annotate |
| Tue, 07 Dec 2010 15:55:35 +0100 |
merged
|
file | diff | annotate |
| Tue, 07 Dec 2010 14:53:44 +0100 |
moved smt_word.ML into the directory of the Word library
|
file | diff | annotate |
| Tue, 07 Dec 2010 09:58:56 +0100 |
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
|
file | diff | annotate |
| Fri, 03 Dec 2010 15:25:14 +0100 |
it is known as the extended reals, not the infinite reals
|
file | diff | annotate |
| Mon, 06 Dec 2010 09:25:05 +0100 |
moved bootstrap of type_lifting to Fun
|
file | diff | annotate |
| Mon, 06 Dec 2010 09:19:10 +0100 |
replace `type_mapper` by the more adequate `type_lifting`
|
file | diff | annotate |
| Fri, 03 Dec 2010 17:59:13 +0100 |
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 |
Corrected IsaMakefile
|
file | diff | annotate |
| Wed, 01 Dec 2010 19:36:05 +0100 |
merged
|
file | diff | annotate |
| Wed, 01 Dec 2010 19:27:53 +0100 |
More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability.
|
file | diff | annotate |
| Wed, 01 Dec 2010 18:00:40 +0100 |
merged
|
file | diff | annotate |
| Wed, 01 Dec 2010 11:33:17 +0100 |
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 |
activate subtyping/coercions in theory Complex_Main;
|
file | diff | annotate |
| Wed, 01 Dec 2010 11:01:20 +0100 |
more precise dependencies;
|
file | diff | annotate |
| Sat, 27 Nov 2010 17:44:36 -0800 |
fix cut-and-paste errors for HOLCF entries in IsaMakefile
|
file | diff | annotate |
| Sat, 27 Nov 2010 16:08:10 -0800 |
moved directory src/HOLCF to src/HOL/HOLCF;
|
file | diff | annotate |
| Tue, 23 Nov 2010 23:11:06 +0100 |
merged
|
file | diff | annotate |
| Mon, 22 Nov 2010 17:49:12 +0100 |
merged
|
file | diff | annotate |