src/HOL/IsaMakefile
Fri, 11 Mar 2011 10:37:36 +0100 bulwahn adding Lazysmallcheck prototype to HOL-Library
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;
Sat, 26 Feb 2011 20:16:44 +0100 nipkow Corrected HOLCF/FOCUS dependency
Sat, 26 Feb 2011 16:16:36 +0100 nipkow corrected HOLCF dependency on Nat_Infinity
Wed, 23 Feb 2011 11:23:26 +0100 noschinl setup case_product attribute in HOL and FOL
Wed, 19 Jan 2011 11:34:10 +0100 hoelzl merged
Tue, 18 Jan 2011 21:37:23 +0100 hoelzl Gauge measure removed
Sat, 15 Jan 2011 20:05:29 +0100 haftmann experimental variant of interpretation with simultaneous definitions, plus example
Sat, 15 Jan 2011 13:41:58 +0100 berghofe Also added SPARK to test and clean targets.
Sat, 15 Jan 2011 12:48:39 +0100 berghofe Added HOL-SPARK and removed old_primrec.ML
Tue, 11 Jan 2011 14:12:37 +0100 haftmann "enriched_type" replaces less specific "type_lifting"
Mon, 10 Jan 2011 17:37:11 +0100 krauss removed obsolete make target (now in doc-src, cf. 28b487cd9e15)
Sat, 08 Jan 2011 17:39:51 +0100 wenzelm renamed Sum_Of_Squares to Sum_of_Squares;
Fri, 07 Jan 2011 18:10:43 +0100 bulwahn adding example theory for list comprehension to set comprehension simproc
Fri, 07 Jan 2011 18:10:35 +0100 bulwahn adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
Mon, 03 Jan 2011 16:22:08 +0100 boehmes re-implemented support for datatypes (including records and typedefs);
Wed, 29 Dec 2010 17:34:41 +0100 wenzelm explicit file specifications -- avoid secondary load path;
Wed, 29 Dec 2010 12:16:49 +0100 wenzelm made SML/NJ happy;
Tue, 21 Dec 2010 10:24:56 +0100 blanchet renamed "sledgehammer_tactic.ML" to "sledgehammer_tactics.ML" (cf. module name);
Sun, 19 Dec 2010 05:15:31 -0800 huffman reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
Sun, 19 Dec 2010 04:06:02 -0800 huffman renamed Bifinite.thy to Representable.thy
Fri, 17 Dec 2010 16:43:45 -0800 huffman renamed CompactBasis.thy to Compact_Basis.thy
Wed, 15 Dec 2010 11:26:28 +0100 blanchet example tuning
Sat, 11 Dec 2010 21:27:53 -0800 huffman add HOLCF library theories with cpo/predomain instances for HOL types
Wed, 08 Dec 2010 22:17:52 +0100 blanchet split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
Tue, 07 Dec 2010 15:55:35 +0100 boehmes merged
Tue, 07 Dec 2010 14:53:44 +0100 boehmes moved smt_word.ML into the directory of the Word library
Tue, 07 Dec 2010 09:58:56 +0100 blanchet load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
Fri, 03 Dec 2010 15:25:14 +0100 hoelzl it is known as the extended reals, not the infinite reals
Mon, 06 Dec 2010 09:25:05 +0100 haftmann moved bootstrap of type_lifting to Fun
Mon, 06 Dec 2010 09:19:10 +0100 haftmann replace `type_mapper` by the more adequate `type_lifting`
Fri, 03 Dec 2010 17:59:13 +0100 wenzelm setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
Wed, 01 Dec 2010 19:42:09 +0100 hoelzl Corrected IsaMakefile
Wed, 01 Dec 2010 19:36:05 +0100 hoelzl merged
Wed, 01 Dec 2010 19:27:53 +0100 hoelzl More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability.
Wed, 01 Dec 2010 18:00:40 +0100 haftmann merged
Wed, 01 Dec 2010 11:33:17 +0100 haftmann file for package tool type_mapper carries the same name as its Isar command
Wed, 01 Dec 2010 11:32:24 +0100 wenzelm activate subtyping/coercions in theory Complex_Main;
Wed, 01 Dec 2010 11:01:20 +0100 wenzelm more precise dependencies;
Sat, 27 Nov 2010 17:44:36 -0800 huffman fix cut-and-paste errors for HOLCF entries in IsaMakefile
Sat, 27 Nov 2010 16:08:10 -0800 huffman moved directory src/HOLCF to src/HOL/HOLCF;
Tue, 23 Nov 2010 23:11:06 +0100 haftmann merged
Mon, 22 Nov 2010 17:49:12 +0100 haftmann merged
Mon, 22 Nov 2010 17:46:51 +0100 haftmann replaced misleading Fset/fset name -- these do not stand for finite sets
Mon, 22 Nov 2010 15:45:42 +0100 boehmes added prove reconstruction for injective functions;
Mon, 22 Nov 2010 11:34:56 +0100 bulwahn adding Enum to HOL-Main image and removing it from HOL-Library
Mon, 22 Nov 2010 10:41:54 +0100 bulwahn adding dependencies to IsaMakefile; adding sledgehammer_tactic in Mirabelle_Test
Mon, 22 Nov 2010 10:41:52 +0100 bulwahn adding birthday paradoxon from some abandoned drawer
Wed, 17 Nov 2010 11:09:18 +0100 haftmann module for functorial mappers
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)
Mon, 08 Nov 2010 09:25:43 +0100 bulwahn adding code and theory for smallvalue generators, but do not setup the interpretation yet
Thu, 04 Nov 2010 13:37:11 +0100 haftmann merged
Wed, 03 Nov 2010 12:20:33 +0100 haftmann moved theory Quicksort from Library/ to ex/
Thu, 04 Nov 2010 09:53:23 +0100 blanchet moved file in makefile to reflect actual dependencies
Fri, 29 Oct 2010 21:34:07 +0200 wenzelm Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
Fri, 29 Oct 2010 18:17:08 +0200 boehmes added crafted list of SMT built-in constants
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;
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
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
Mon, 25 Oct 2010 21:17:16 +0200 bulwahn adding new predicate compiler files to the IsaMakefile
less more (0) -1000 -300 -100 -60 tip