src/HOL/Quickcheck_Narrowing.thy
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