clarified document antiquotation @{theory};

ran isabelle update_op on all sources

more symbols;

prefer file dependencies wrt. specific theories;

avoid ancient [code, code del] antipattern

--HG--
extra : rebase_source : 84d96ea0a3eb069ee7f5bd2b76c41af692702279

early abort on depth limit

--HG--
extra : rebase_source : 6680bc51d50d9c83f035fcbf3487b684dce780be

obsolete

--HG--
extra : rebase_source : 8f39a49a3888512a75f92b8a8a2433e96327630e

tuned

--HG--
extra : rebase_source : b2ffac74734a56f53d312909c5f13ea1e41577f3

isabelle update_cartouches -c -t;

isabelle update_cartouches;

allow multiple inheritance of targets

--HG--
extra : rebase_source : 9d4980222d189226728427249e77a98373cb2011

modernized header uniformly as section;

modernized setup;

tuned;

always annotate potentially polymorphic Haskell numerals

--HG--
extra : rebase_source : afdd470c78d704a706fe6d34761f4251b2b79ec0

added 'extraction' plugins -- this might help 'HOL-Proofs'

disable datatype 'plugins' for internal types

updated news

use 'datatype_new' in 'Main'

add missing adaptation for narrowing to work with variables of type integer => integer

make it possible to load Quickcheck exhaustive & narrowing in parallel

avoid ad-hoc patching of generated code

prefer explicit code symbol type over ad-hoc name mangling

migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier

--HG--
extra : rebase_source : ff8027ac9606264aa4b2d4f8da037c426a3db98b

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

dropped dead code;
tuned theory text

Renamed {left,right}_distrib to distrib_{right,left}.

discontinued obsolete typedef (open) syntax;

more basic file dependencies -- no load command here;

prefer ML_file over old uses;

restored narrowing quickcheck after 6efff142bb54

a first guess to avoid the Codegenerator_Test to loop infinitely

merged fork with new numeral representation (see NEWS)

declare command keywords via theory header, including strict checking outside Pure;

choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing

adding new command "find_unused_assms"

adding narrowing instance for sets

dropped redundant setup

--HG--
extra : rebase_source : ca966376aba0c4fd10f2a39d7672f26b935bdbcc

hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;

hide quickcheck constants Abs_cfun and Rep_cfun, to avoid clash with HOLCF

ensuring that some constants are generated in the source code by adding calls in ensure_testable

adding narrowing instances for real and rational

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;

hide rather short auxiliary names, which can easily occur in user theories;

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;

removed comment and declaration after issue has been resolved (cf. e83695ea0e0a)

adding another narrowing strategy for integers

fixed document generation for HOL

fixing code generation test

removing char setup

removing unneccessary manual instantiations and dead definitions; hiding more constants and facts

adding a nicer error message for quickcheck_narrowing; hiding fact empty_def

adapting Quickcheck_Narrowing: adding setup for characters; correcting import statement

moving Quickcheck_Narrowing from Library to base directory

--HG--
rename : src/HOL/Library/Quickcheck_Narrowing.thy => src/HOL/Quickcheck_Narrowing.thy