src/HOL/IsaMakefile
Fri, 22 Jan 2010 13:38:29 +0100 haftmann more accurate dependencies
Sat, 02 Jan 2010 23:18:58 +0100 krauss absorb structures Decompose and Descent into Termination, to simplify further restructuring
Tue, 29 Dec 2009 16:20:39 +0100 wenzelm explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
Fri, 18 Dec 2009 12:00:29 +0100 blanchet polished Nitpick's binary integer support etc.;
Fri, 11 Dec 2009 15:36:05 +0100 boehmes updated dependencies
Fri, 11 Dec 2009 15:06:12 +0100 boehmes depend on HOL-SMT instead of HOL (makes tactic "smt" available for proofs)
Mon, 07 Dec 2009 16:27:48 +0100 haftmann split off evaluation mechanisms in separte module Code_Eval
Mon, 07 Dec 2009 14:54:01 +0100 haftmann merged Crude_Executable_Set into Executable_Set
Fri, 04 Dec 2009 12:22:09 +0100 haftmann merged
Mon, 30 Nov 2009 11:42:49 +0100 haftmann modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
Fri, 27 Nov 2009 08:41:10 +0100 haftmann renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
Tue, 24 Nov 2009 14:37:23 +0100 haftmann backported parts of abstract byte code verifier from AFP/Jinja
Wed, 02 Dec 2009 17:53:34 +0100 haftmann added Crude_Executable_Set.thy
Fri, 20 Nov 2009 15:33:10 +0100 wenzelm load ML directly into theory Code_Generator (quickcheck also requires this);
Wed, 18 Nov 2009 09:34:53 +0100 boehmes added arithmetic example using div and mod
Tue, 17 Nov 2009 18:52:30 +0100 hoelzl Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
Sat, 14 Nov 2009 19:56:18 +0100 wenzelm moved old SList, LList, LFilter to AFP/Lazy-Lists-II;
Thu, 12 Nov 2009 20:38:57 +0100 bulwahn added a tabled implementation of the reflexive transitive closure
Tue, 10 Nov 2009 13:54:00 +0100 blanchet merged, and renamed local "TheoryData" to "Data" (following common Isabelle conventions)
Thu, 05 Nov 2009 11:58:36 +0100 blanchet merged
Thu, 29 Oct 2009 23:08:51 +0100 blanchet merged
Thu, 29 Oct 2009 15:26:00 +0100 blanchet merged
Thu, 29 Oct 2009 12:09:32 +0100 blanchet merged
Wed, 28 Oct 2009 18:09:30 +0100 blanchet merged my Auto Nitpick change with Lukas's Predicate Compiler changes
Wed, 28 Oct 2009 17:43:43 +0100 blanchet introduced Auto Nitpick in addition to Auto Quickcheck;
Mon, 09 Nov 2009 15:50:15 +0000 paulson New theory Probability/Borel.thy, and some associated lemmas
Fri, 06 Nov 2009 14:42:42 +0100 krauss renamed method induct_scheme to induction_schema
Fri, 06 Nov 2009 13:42:29 +0100 krauss removed session SizeChange: outdated, only half-functional, alternatives exist (cf. size_change method)
Thu, 05 Nov 2009 16:23:51 +0100 wenzelm more accurate cleanup;
Thu, 05 Nov 2009 15:55:07 +0100 wenzelm merged
Thu, 05 Nov 2009 15:54:14 +0100 wenzelm more accurate dependencies;
Thu, 05 Nov 2009 15:44:39 +0100 boehmes merged
Thu, 05 Nov 2009 15:24:49 +0100 boehmes handle let expressions inside terms by unfolding (instead of raising an exception),
Thu, 05 Nov 2009 14:48:40 +0100 boehmes shorter names for variables and verification conditions,
Thu, 05 Nov 2009 14:37:39 +0100 wenzelm more accurate dependencies;
Wed, 04 Nov 2009 17:17:30 +0100 krauss added Tree23 to IsaMakefile
Tue, 03 Nov 2009 17:54:24 +0100 boehmes added HOL-Boogie
Fri, 30 Oct 2009 13:59:49 +0100 haftmann moved Commutative_Ring into session Decision_Procs
Fri, 30 Oct 2009 01:32:06 +0100 krauss absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
Thu, 29 Oct 2009 18:17:26 +0100 wenzelm merged
Thu, 29 Oct 2009 11:41:36 +0100 haftmann moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
Thu, 29 Oct 2009 16:06:15 +0100 wenzelm separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
Thu, 29 Oct 2009 08:14:39 +0100 haftmann merged
Wed, 28 Oct 2009 19:09:47 +0100 haftmann moved theory Divides after theory Nat_Numeral; tuned some proof texts
Wed, 28 Oct 2009 18:21:02 +0100 wenzelm tuned;
Wed, 28 Oct 2009 11:43:06 +0000 paulson merged
Wed, 28 Oct 2009 11:42:31 +0000 paulson New theory Probability, which contains a development of measure theory
Tue, 27 Oct 2009 14:46:03 +0000 paulson merged
Tue, 27 Oct 2009 12:59:57 +0000 paulson New theory SupInf of the supremum and infimum operators for sets of reals.
Tue, 27 Oct 2009 19:03:59 +0100 bulwahn merged
Tue, 27 Oct 2009 09:03:56 +0100 bulwahn adding a prototype of a counter-example generator based on the predicate compiler to HOL/ex
Tue, 27 Oct 2009 09:02:22 +0100 bulwahn including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
Tue, 27 Oct 2009 18:09:11 +0100 boehmes removed unused file smt_builtin.ML,
Mon, 26 Oct 2009 20:04:20 +0100 wenzelm recovered sort indentation for "sort position", as documented in the file;
Mon, 26 Oct 2009 14:57:49 +0100 blanchet merged
Mon, 26 Oct 2009 14:21:20 +0100 blanchet merged
Mon, 26 Oct 2009 09:14:29 +0100 blanchet merged
Fri, 23 Oct 2009 18:59:24 +0200 blanchet continuation of Nitpick's integration into Isabelle;
Thu, 22 Oct 2009 14:51:47 +0200 blanchet added Nitpick's theory and ML files to Isabelle/HOL;
Mon, 26 Oct 2009 14:54:43 +0100 berghofe merged
less more (0) -1000 -300 -100 -60 tip