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