src/HOL/Quickcheck_Narrowing.thy
Sat, 19 Jan 2019 07:19:16 +0000 haftmann self-contained code modules for Haskell
Sun, 06 Jan 2019 15:04:34 +0100 wenzelm isabelle update -u path_cartouches;
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Sat, 29 Dec 2018 09:28:30 +0000 haftmann explicit dependencies for includes
Fri, 22 Jun 2018 20:31:49 +0200 wenzelm clarified document antiquotation @{theory};
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Sun, 26 Nov 2017 21:08:32 +0100 wenzelm more symbols;
Mon, 02 Oct 2017 19:38:39 +0200 wenzelm prefer file dependencies wrt. specific theories;
Tue, 20 Jun 2017 13:07:47 +0200 haftmann avoid ancient [code, code del] antipattern
Thu, 13 Apr 2017 10:10:09 +0200 haftmann early abort on depth limit
Thu, 13 Apr 2017 10:10:08 +0200 haftmann obsolete
Thu, 13 Apr 2017 10:10:06 +0200 haftmann tuned
Mon, 07 Dec 2015 10:38:04 +0100 wenzelm isabelle update_cartouches -c -t;
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Fri, 05 Dec 2014 19:35:36 +0100 haftmann allow multiple inheritance of targets
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Wed, 29 Oct 2014 19:01:49 +0100 wenzelm modernized setup;
Wed, 29 Oct 2014 11:19:27 +0100 wenzelm tuned;
Thu, 18 Sep 2014 18:48:54 +0200 haftmann always annotate potentially polymorphic Haskell numerals
Tue, 16 Sep 2014 19:23:37 +0200 blanchet added 'extraction' plugins -- this might help 'HOL-Proofs'
Sun, 14 Sep 2014 22:59:30 +0200 blanchet disable datatype 'plugins' for internal types
Thu, 11 Sep 2014 19:32:36 +0200 blanchet updated news
Wed, 03 Sep 2014 00:06:24 +0200 blanchet use 'datatype_new' in 'Main'
Fri, 04 Apr 2014 13:22:15 +0200 Andreas Lochbihler add missing adaptation for narrowing to work with variables of type integer => integer
Tue, 11 Mar 2014 17:18:39 +0100 blanchet make it possible to load Quickcheck exhaustive & narrowing in parallel
Sun, 23 Feb 2014 10:33:43 +0100 haftmann avoid ad-hoc patching of generated code
Sat, 25 Jan 2014 23:50:49 +0100 haftmann prefer explicit code symbol type over ad-hoc name mangling
Sun, 23 Jun 2013 21:16:07 +0200 haftmann migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
Fri, 15 Feb 2013 08:31:31 +0100 haftmann two target language numeral types: integer and natural, as replacement for code_numeral;
Sun, 11 Nov 2012 19:56:02 +0100 haftmann dropped dead code;
Fri, 19 Oct 2012 15:12:52 +0200 webertj Renamed {left,right}_distrib to distrib_{right,left}.
Fri, 12 Oct 2012 18:58:20 +0200 wenzelm discontinued obsolete typedef (open) syntax;
Thu, 23 Aug 2012 12:55:23 +0200 wenzelm more basic file dependencies -- no load command here;
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Fri, 27 Jul 2012 20:05:56 +0200 haftmann restored narrowing quickcheck after 6efff142bb54
Thu, 12 Jul 2012 16:22:33 +0200 bulwahn a first guess to avoid the Codegenerator_Test to loop infinitely
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
Thu, 15 Mar 2012 22:08:53 +0100 wenzelm declare command keywords via theory header, including strict checking outside Pure;
Fri, 02 Mar 2012 09:35:35 +0100 bulwahn choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
Wed, 22 Feb 2012 17:22:53 +0100 bulwahn adding new command "find_unused_assms"
Fri, 20 Jan 2012 09:28:53 +0100 bulwahn adding narrowing instance for sets
Thu, 29 Dec 2011 10:47:56 +0100 haftmann dropped redundant setup
Mon, 12 Dec 2011 13:45:54 +0100 bulwahn hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
Fri, 02 Dec 2011 10:31:47 +0100 huffman hide quickcheck constants Abs_cfun and Rep_cfun, to avoid clash with HOLCF
Mon, 19 Sep 2011 16:18:30 +0200 bulwahn ensuring that some constants are generated in the source code by adding calls in ensure_testable
Mon, 18 Jul 2011 10:34:21 +0200 bulwahn adding narrowing instances for real and rational
Fri, 08 Jul 2011 14:37:19 +0200 wenzelm more abstract Thy_Load.load_file/use_file for external theory resources;
Mon, 27 Jun 2011 17:20:24 +0200 wenzelm hide rather short auxiliary names, which can easily occur in user theories;
Sat, 25 Jun 2011 14:25:10 +0200 wenzelm removed very slow proof of unnamed/unused theorem from HOL/Quickcheck_Narrowing.thy (cf. 2dee03f192b7) -- can take seconds for main HOL and minutes for HOL-Proofs;
Tue, 14 Jun 2011 08:30:18 +0200 bulwahn removed comment and declaration after issue has been resolved (cf. e83695ea0e0a)
Fri, 10 Jun 2011 15:42:21 +0200 bulwahn adding another narrowing strategy for integers
Thu, 09 Jun 2011 14:04:38 +0200 hoelzl fixed document generation for HOL
Thu, 09 Jun 2011 09:07:13 +0200 bulwahn fixing code generation test
Thu, 09 Jun 2011 08:32:22 +0200 bulwahn removing char setup
Thu, 09 Jun 2011 08:32:21 +0200 bulwahn removing unneccessary manual instantiations and dead definitions; hiding more constants and facts
Thu, 09 Jun 2011 08:32:19 +0200 bulwahn adding a nicer error message for quickcheck_narrowing; hiding fact empty_def
Thu, 09 Jun 2011 08:32:18 +0200 bulwahn adapting Quickcheck_Narrowing: adding setup for characters; correcting import statement
Thu, 09 Jun 2011 08:32:14 +0200 bulwahn moving Quickcheck_Narrowing from Library to base directory
less more (0) tip