#
e10c04e8 |
|
19-Jan-2019 |
haftmann <none@none> |
self-contained code modules for Haskell --HG-- extra : rebase_source : a3b1eacb5c9dd9b269251b2329a9eed2ec8eb2da
|
#
e60cf64d |
|
06-Jan-2019 |
wenzelm <none@none> |
isabelle update -u path_cartouches;
|
#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
dd5fe348 |
|
29-Dec-2018 |
haftmann <none@none> |
explicit dependencies for includes
|
#
8413f38b |
|
22-Jun-2018 |
wenzelm <none@none> |
clarified document antiquotation @{theory};
|
#
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
#
c7cc1919 |
|
26-Nov-2017 |
wenzelm <none@none> |
more symbols;
|
#
415ab5f1 |
|
02-Oct-2017 |
wenzelm <none@none> |
prefer file dependencies wrt. specific theories;
|
#
bb40207a |
|
20-Jun-2017 |
haftmann <none@none> |
avoid ancient [code, code del] antipattern --HG-- extra : rebase_source : 84d96ea0a3eb069ee7f5bd2b76c41af692702279
|
#
9b7ca132 |
|
13-Apr-2017 |
haftmann <none@none> |
early abort on depth limit --HG-- extra : rebase_source : 6680bc51d50d9c83f035fcbf3487b684dce780be
|
#
36912715 |
|
13-Apr-2017 |
haftmann <none@none> |
obsolete --HG-- extra : rebase_source : 8f39a49a3888512a75f92b8a8a2433e96327630e
|
#
e68387ad |
|
13-Apr-2017 |
haftmann <none@none> |
tuned --HG-- extra : rebase_source : b2ffac74734a56f53d312909c5f13ea1e41577f3
|
#
0df376fc |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
#
0976a200 |
|
05-Dec-2014 |
haftmann <none@none> |
allow multiple inheritance of targets --HG-- extra : rebase_source : 9d4980222d189226728427249e77a98373cb2011
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
f9cb1a7a |
|
29-Oct-2014 |
wenzelm <none@none> |
modernized setup;
|
#
ae3211cd |
|
29-Oct-2014 |
wenzelm <none@none> |
tuned;
|
#
5f477322 |
|
18-Sep-2014 |
haftmann <none@none> |
always annotate potentially polymorphic Haskell numerals --HG-- extra : rebase_source : afdd470c78d704a706fe6d34761f4251b2b79ec0
|
#
1e04f9e5 |
|
16-Sep-2014 |
blanchet <none@none> |
added 'extraction' plugins -- this might help 'HOL-Proofs'
|
#
3c8247b0 |
|
14-Sep-2014 |
blanchet <none@none> |
disable datatype 'plugins' for internal types
|
#
5fc26177 |
|
11-Sep-2014 |
blanchet <none@none> |
updated news
|
#
1ba740de |
|
02-Sep-2014 |
blanchet <none@none> |
use 'datatype_new' in 'Main'
|
#
7bff6238 |
|
04-Apr-2014 |
Andreas Lochbihler <none@none> |
add missing adaptation for narrowing to work with variables of type integer => integer
|
#
beb8c069 |
|
11-Mar-2014 |
blanchet <none@none> |
make it possible to load Quickcheck exhaustive & narrowing in parallel
|
#
2091c516 |
|
23-Feb-2014 |
haftmann <none@none> |
avoid ad-hoc patching of generated code
|
#
9250249f |
|
25-Jan-2014 |
haftmann <none@none> |
prefer explicit code symbol type over ad-hoc name mangling
|
#
a7b3de52 |
|
23-Jun-2013 |
haftmann <none@none> |
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier --HG-- extra : rebase_source : ff8027ac9606264aa4b2d4f8da037c426a3db98b
|
#
5a8927d0 |
|
15-Feb-2013 |
haftmann <none@none> |
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 --HG-- extra : rebase_source : ffa0242ad108fe680ff144a716257c0784285d17
|
#
2d9c32f8 |
|
11-Nov-2012 |
haftmann <none@none> |
dropped dead code; tuned theory text
|
#
d9333ba5 |
|
19-Oct-2012 |
webertj <none@none> |
Renamed {left,right}_distrib to distrib_{right,left}.
|
#
c82bd4c5 |
|
12-Oct-2012 |
wenzelm <none@none> |
discontinued obsolete typedef (open) syntax;
|
#
3f40e702 |
|
22-Aug-2012 |
wenzelm <none@none> |
more basic file dependencies -- no load command here;
|
#
e3227796 |
|
22-Aug-2012 |
wenzelm <none@none> |
prefer ML_file over old uses;
|
#
7b8fa900 |
|
27-Jul-2012 |
haftmann <none@none> |
restored narrowing quickcheck after 6efff142bb54
|
#
c99b1333 |
|
12-Jul-2012 |
bulwahn <none@none> |
a first guess to avoid the Codegenerator_Test to loop infinitely
|
#
8bb6233a |
|
25-Mar-2012 |
huffman <none@none> |
merged fork with new numeral representation (see NEWS)
|
#
870593bf |
|
15-Mar-2012 |
wenzelm <none@none> |
declare command keywords via theory header, including strict checking outside Pure;
|
#
16a2ce8b |
|
02-Mar-2012 |
bulwahn <none@none> |
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
|
#
d75b0b6b |
|
22-Feb-2012 |
bulwahn <none@none> |
adding new command "find_unused_assms"
|
#
c127dfd5 |
|
20-Jan-2012 |
bulwahn <none@none> |
adding narrowing instance for sets
|
#
e707bb63 |
|
29-Dec-2011 |
haftmann <none@none> |
dropped redundant setup --HG-- extra : rebase_source : ca966376aba0c4fd10f2a39d7672f26b935bdbcc
|
#
73beb7c3 |
|
12-Dec-2011 |
bulwahn <none@none> |
hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
|
#
1b8c1021 |
|
02-Dec-2011 |
huffman <none@none> |
hide quickcheck constants Abs_cfun and Rep_cfun, to avoid clash with HOLCF
|
#
6ea898c5 |
|
19-Sep-2011 |
bulwahn <none@none> |
ensuring that some constants are generated in the source code by adding calls in ensure_testable
|
#
e0616246 |
|
18-Jul-2011 |
bulwahn <none@none> |
adding narrowing instances for real and rational
|
#
1c7e4887 |
|
08-Jul-2011 |
wenzelm <none@none> |
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;
|
#
a89ca2c7 |
|
27-Jun-2011 |
wenzelm <none@none> |
hide rather short auxiliary names, which can easily occur in user theories;
|
#
e35f093a |
|
25-Jun-2011 |
wenzelm <none@none> |
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;
|
#
b0a5aa10 |
|
14-Jun-2011 |
bulwahn <none@none> |
removed comment and declaration after issue has been resolved (cf. e83695ea0e0a)
|
#
d724bb33 |
|
10-Jun-2011 |
bulwahn <none@none> |
adding another narrowing strategy for integers
|
#
c8c2b82d |
|
09-Jun-2011 |
hoelzl <none@none> |
fixed document generation for HOL
|
#
4abac951 |
|
09-Jun-2011 |
bulwahn <none@none> |
fixing code generation test
|
#
a8a9e210 |
|
09-Jun-2011 |
bulwahn <none@none> |
removing char setup
|
#
c43eedf7 |
|
09-Jun-2011 |
bulwahn <none@none> |
removing unneccessary manual instantiations and dead definitions; hiding more constants and facts
|
#
b77eb80b |
|
09-Jun-2011 |
bulwahn <none@none> |
adding a nicer error message for quickcheck_narrowing; hiding fact empty_def
|
#
ff3157bc |
|
09-Jun-2011 |
bulwahn <none@none> |
adapting Quickcheck_Narrowing: adding setup for characters; correcting import statement
|
#
d83d143d |
|
09-Jun-2011 |
bulwahn <none@none> |
moving Quickcheck_Narrowing from Library to base directory --HG-- rename : src/HOL/Library/Quickcheck_Narrowing.thy => src/HOL/Quickcheck_Narrowing.thy
|