src/HOL/Quickcheck_Narrowing.thy
2014-01-25 haftmann 2014-01-25 prefer explicit code symbol type over ad-hoc name mangling
2013-06-23 haftmann 2013-06-23 migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
2013-02-15 haftmann 2013-02-15 two target language numeral types: integer and natural, as replacement for code_numeral; former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral; refined stack of theories implementing int and/or nat by target language numerals; reduced number of target language numeral types to exactly one
2012-11-11 haftmann 2012-11-11 dropped dead code; tuned theory text
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2012-08-23 wenzelm 2012-08-23 more basic file dependencies -- no load command here;
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-07-27 haftmann 2012-07-27 restored narrowing quickcheck after 6efff142bb54
2012-07-12 bulwahn 2012-07-12 a first guess to avoid the Codegenerator_Test to loop infinitely
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-03-15 wenzelm 2012-03-15 declare command keywords via theory header, including strict checking outside Pure;
2012-03-02 bulwahn 2012-03-02 choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
2012-02-22 bulwahn 2012-02-22 adding new command "find_unused_assms"
2012-01-20 bulwahn 2012-01-20 adding narrowing instance for sets
2011-12-29 haftmann 2011-12-29 dropped redundant setup
2011-12-12 bulwahn 2011-12-12 hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
2011-12-02 huffman 2011-12-02 hide quickcheck constants Abs_cfun and Rep_cfun, to avoid clash with HOLCF
2011-09-19 bulwahn 2011-09-19 ensuring that some constants are generated in the source code by adding calls in ensure_testable
2011-07-18 bulwahn 2011-07-18 adding narrowing instances for real and rational
2011-07-08 wenzelm 2011-07-08 more abstract Thy_Load.load_file/use_file for external theory resources; prefer Boogie_Loader.parse_b2i on already loaded text, bypassing former File.fold_lines optimization;
2011-06-27 wenzelm 2011-06-27 hide rather short auxiliary names, which can easily occur in user theories;
2011-06-25 wenzelm 2011-06-25 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 2011-06-14 removed comment and declaration after issue has been resolved (cf. e83695ea0e0a)
2011-06-10 bulwahn 2011-06-10 adding another narrowing strategy for integers
2011-06-09 hoelzl 2011-06-09 fixed document generation for HOL
2011-06-09 bulwahn 2011-06-09 fixing code generation test
2011-06-09 bulwahn 2011-06-09 removing char setup
2011-06-09 bulwahn 2011-06-09 removing unneccessary manual instantiations and dead definitions; hiding more constants and facts
2011-06-09 bulwahn 2011-06-09 adding a nicer error message for quickcheck_narrowing; hiding fact empty_def
2011-06-09 bulwahn 2011-06-09 adapting Quickcheck_Narrowing: adding setup for characters; correcting import statement
2011-06-09 bulwahn 2011-06-09 moving Quickcheck_Narrowing from Library to base directory