src/HOL/IsaMakefile
Thu, 11 Aug 2011 09:41:21 +0200 krauss removed obsolete recdef-related examples
Wed, 10 Aug 2011 20:12:36 +0200 wenzelm moved old code generator to src/Tools/;
Tue, 09 Aug 2011 09:05:21 +0200 blanchet load lambda-lifting structure earlier, so it can be used in Metis
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
Tue, 02 Aug 2011 10:36:50 +0200 krauss moved recdef package to HOL/Library/Old_Recdef.thy
Mon, 01 Aug 2011 09:31:10 -0700 huffman new theory HOL/Library/Product_Lattice.thy
Tue, 26 Jul 2011 18:11:38 +0200 bulwahn more precise dependencies
Mon, 25 Jul 2011 10:43:14 +0200 bulwahn removing SML_Quickcheck
Wed, 20 Jul 2011 13:29:54 +0200 boehmes more precise dependencies
Wed, 20 Jul 2011 13:27:01 +0200 boehmes merged
Wed, 20 Jul 2011 09:23:09 +0200 boehmes removed old (unused) SMT monomorphizer
Wed, 20 Jul 2011 10:48:00 +0200 hoelzl merged
Tue, 19 Jul 2011 14:36:12 +0200 hoelzl Rename extreal => ereal
Tue, 19 Jul 2011 14:35:44 +0200 hoelzl rename Nat_Infinity (inat) to Extended_Nat (enat)
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.
Wed, 20 Jul 2011 08:46:17 +0200 kleing build an image for HOL-IMP
Thu, 14 Jul 2011 22:08:11 +0200 krauss added missing dependencies;
Wed, 13 Jul 2011 22:16:19 +0200 blanchet cleanly separate TPTP related files from other examples
Wed, 13 Jul 2011 15:50:45 +0200 krauss experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
Wed, 06 Jul 2011 17:19:34 +0100 blanchet moved ATP dependencies to HOL-Plain, where they belong
Fri, 01 Jul 2011 11:26:02 +0200 bulwahn improving actual dependencies
Mon, 27 Jun 2011 09:42:46 +0200 hoelzl move conditional expectation to its own theory file
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
Fri, 17 Jun 2011 20:38:43 +0200 kleing IMP compiler with int, added reverse soundness direction
Thu, 09 Jun 2011 08:32:15 +0200 bulwahn adapting IsaMakefile
Tue, 07 Jun 2011 11:24:16 +0200 bulwahn merged; manually merged IsaMakefile
Tue, 07 Jun 2011 11:12:05 +0200 bulwahn splitting Cset into Cset and List_Cset
Tue, 07 Jun 2011 11:10:57 +0200 bulwahn renaming the formalisation of the birthday problem to a proper English name
Tue, 07 Jun 2011 07:04:53 +0200 blanchet renamed example theory to "ATP_Export", for consistency with its underlying "ATP_" modules
Mon, 06 Jun 2011 20:36:35 +0200 blanchet tuned Metis examples
Mon, 06 Jun 2011 20:36:34 +0200 blanchet added Metis examples to test the new type encodings
Mon, 06 Jun 2011 16:29:38 +0200 kleing imported rest of new IMP
Thu, 02 Jun 2011 10:10:23 +0200 nipkow Added typed IMP
Thu, 02 Jun 2011 08:55:08 +0200 bulwahn splitting Dlist theory in Dlist and Dlist_Cset
Wed, 01 Jun 2011 21:50:49 +0200 nipkow Removed old IMP files
Wed, 01 Jun 2011 09:10:13 +0200 bulwahn splitting RBT theory into RBT and RBT_Mapping
Tue, 31 May 2011 16:38:36 +0200 blanchet use "monomorph.ML" in "ATP" theory (so the new Metis can use it)
Tue, 31 May 2011 16:38:36 +0200 blanchet first step in sharing more code between ATP and Metis translation
Fri, 27 May 2011 10:30:08 +0200 blanchet renamed "Auto_Tools" "Try"
Fri, 27 May 2011 10:30:08 +0200 blanchet renamed "try" "try_methods"
Tue, 17 May 2011 11:47:36 +0200 hoelzl Add formalization of probabilistic independence for families of sets
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
Mon, 02 May 2011 12:09:33 +0200 blanchet added TPTP exporter facility -- useful to do experiments with machine learning
Mon, 02 May 2011 12:09:33 +0200 blanchet renamed theory to make its purpose clearer
Thu, 14 Apr 2011 11:24:05 +0200 blanchet compile
Thu, 14 Apr 2011 11:24:04 +0200 blanchet started clausifier examples
Wed, 30 Mar 2011 10:31:02 +0200 bulwahn adding a regression test for SML_Quickcheck; putting SML_Quickcheck back in shape
Tue, 29 Mar 2011 21:48:01 +0200 wenzelm use shared copy of hoare_syntax.ML;
Tue, 29 Mar 2011 14:27:42 +0200 hoelzl rename Probability_Space to Probability_Measure
Tue, 29 Mar 2011 14:27:41 +0200 hoelzl add infinite product measure
Tue, 29 Mar 2011 14:27:39 +0200 hoelzl split Product_Measure into Binary_Product_Measure and Finite_Product_Measure
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";
Wed, 23 Mar 2011 10:06:27 +0100 blanchet move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
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
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
Mon, 21 Mar 2011 14:25:59 +0100 krauss more precise dependencies
Mon, 21 Mar 2011 12:43:26 +0100 krauss small test case for main mirabelle functionality, which easily breaks without noticing
Mon, 14 Mar 2011 14:37:49 +0100 hoelzl reworked Probability theory: measures are not type restricted to positive extended reals
Mon, 14 Mar 2011 14:37:47 +0100 hoelzl split Extended_Reals into parts for Library and Multivariate_Analysis
Mon, 14 Mar 2011 14:37:39 +0100 hoelzl add Extended_Reals from AFP/Lower_Semicontinuous
less more (0) -1000 -300 -100 -60 tip