src/HOL/Quickcheck_Narrowing.thy
2015-12-07 wenzelm isabelle update_cartouches -c -t;
2015-07-18 wenzelm isabelle update_cartouches;
2014-12-05 haftmann allow multiple inheritance of targets
2014-11-02 wenzelm modernized header uniformly as section;
2014-10-29 wenzelm modernized setup;
2014-10-29 wenzelm tuned;
2014-09-18 haftmann always annotate potentially polymorphic Haskell numerals
2014-09-16 blanchet added 'extraction' plugins -- this might help 'HOL-Proofs'
2014-09-14 blanchet disable datatype 'plugins' for internal types
2014-09-11 blanchet updated news
2014-09-02 blanchet use 'datatype_new' in 'Main'
2014-04-04 Andreas Lochbihler add missing adaptation for narrowing to work with variables of type integer => integer
2014-03-11 blanchet make it possible to load Quickcheck exhaustive & narrowing in parallel
2014-02-23 haftmann avoid ad-hoc patching of generated code
2014-01-25 haftmann prefer explicit code symbol type over ad-hoc name mangling
2013-06-23 haftmann migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
2013-02-15 haftmann two target language numeral types: integer and natural, as replacement for code_numeral;
2012-11-11 haftmann dropped dead code;
2012-10-19 webertj Renamed {left,right}_distrib to distrib_{right,left}.
2012-10-12 wenzelm discontinued obsolete typedef (open) syntax;
2012-08-23 wenzelm more basic file dependencies -- no load command here;
2012-08-22 wenzelm prefer ML_file over old uses;
2012-07-27 haftmann restored narrowing quickcheck after 6efff142bb54
2012-07-12 bulwahn a first guess to avoid the Codegenerator_Test to loop infinitely
2012-03-25 huffman merged fork with new numeral representation (see NEWS)
2012-03-15 wenzelm declare command keywords via theory header, including strict checking outside Pure;
2012-03-02 bulwahn choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
2012-02-22 bulwahn adding new command "find_unused_assms"
2012-01-20 bulwahn adding narrowing instance for sets
2011-12-29 haftmann dropped redundant setup
2011-12-12 bulwahn hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
2011-12-02 huffman hide quickcheck constants Abs_cfun and Rep_cfun, to avoid clash with HOLCF
2011-09-19 bulwahn ensuring that some constants are generated in the source code by adding calls in ensure_testable
2011-07-18 bulwahn adding narrowing instances for real and rational
2011-07-08 wenzelm more abstract Thy_Load.load_file/use_file for external theory resources;
2011-06-27 wenzelm hide rather short auxiliary names, which can easily occur in user theories;
2011-06-25 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;
2011-06-14 bulwahn removed comment and declaration after issue has been resolved (cf. e83695ea0e0a)
2011-06-10 bulwahn adding another narrowing strategy for integers
2011-06-09 hoelzl fixed document generation for HOL
2011-06-09 bulwahn fixing code generation test
2011-06-09 bulwahn removing char setup
2011-06-09 bulwahn removing unneccessary manual instantiations and dead definitions; hiding more constants and facts
2011-06-09 bulwahn adding a nicer error message for quickcheck_narrowing; hiding fact empty_def
2011-06-09 bulwahn adapting Quickcheck_Narrowing: adding setup for characters; correcting import statement
2011-06-09 bulwahn moving Quickcheck_Narrowing from Library to base directory
less more (0) tip