proper datatype for 8-bit characters

streamlined code setup for fake terms

--HG--
extra : rebase_source : ef86accead7e67a7aee552c92c5306c6bbf34d86

clarified modules;

--HG--
rename : src/HOL/Tools/value.ML => src/HOL/Tools/value_command.ML

delegate inclusion of required dictionaries to user-space instead of half-working magic

Type_Infer.object_logic controls improvement of type inference result;

model characters directly as range 0..255
* * *
operate on syntax terms rather than asts

isabelle update_cartouches -c -t;

eliminated \<Colon>;

isabelle update_cartouches;

slightly more standard code setup for String.literal, with explicit special case in predicate compiler

modernized header uniformly as section;

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

disable datatype 'plugins' for internal types

updated news

use 'datatype_new' in 'Main'

add code equation for term_of on integer

correct code equation for term_of on integer

dropped term_of obfuscation -- not really required;
tuned theory structure

hardcoded nbe and sml into value command

modernized setups

degeneralized value command into HOL

--HG--
rename : src/Tools/value.ML => src/HOL/Tools/value.ML

more qualified names;

adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'

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

--HG--
extra : rebase_source : ff8027ac9606264aa4b2d4f8da037c426a3db98b

make reification part of HOL

--HG--
rename : src/HOL/Tools/reflection.ML => src/HOL/Tools/reification.ML
extra : rebase_source : 16e93aafd01e25dc85b597f0e457983c2b9cfe1b

syntax translations always depend on context;

systematic conversions between nat and nibble/char;
more uniform approaches to execute operations on nibble/char

--HG--
extra : rebase_source : 982810ecce9e31070e2293715ed744c3b68ae21d

less customary term_of conversions;
spurious side effect on method reflection

--HG--
extra : rebase_source : e98673d202c69d48235f67e609bfe8d39d2ec105

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

reform of predicate compiler / quickcheck theories:
implement yieldn operations uniformly on the ML level -- predicate compiler uses negative integers as parameter to yieldn, whereas code_numeral represents natural numbers!
avoid odd New_ prefix by joining related theories;
avoid overcompact name DSequence;
separated predicate inside random monad into separate theory;
consolidated name of theory Quickcheck

--HG--
rename : src/HOL/DSequence.thy => src/HOL/Limited_Sequence.thy
rename : src/HOL/Quickcheck.thy => src/HOL/Quickcheck_Random.thy
extra : rebase_source : b6adaac1637d6d1cc809d2f937ae890fcc21969c

abandoned theory Plain

--HG--
extra : rebase_source : 6f5a395a55e8879386d1f79ab252c6fc2aca7dc5

tuned import order

prefer ML_file over old uses;

merged fork with new numeral representation (see NEWS)

moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy

--HG--
extra : rebase_source : ed15629634477aff0a8efea30547f496c70907ad

moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy

extending terms of Code_Evaluation by Free to allow partial terms

corrected representation for code_numeral numerals

separate term_of function for integers -- more canonical representation of negative integers

adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict

dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term

Factored out ML into separate file

adjusted to changes in Code_Runtime

Code_Runtime.value, corresponding to ML_Context.value

code_eval renamed to code_runtime

--HG--
rename : src/Tools/Code/code_eval.ML => src/Tools/Code/code_runtime.ML

replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures

fiddling with the correct setup for String.literal

renamed class/constant eq to equal; tuned some instantiations

moved instantiation target formally to class_target.ML

replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;

renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;

evaluation for abstypes

proper distinction of code datatypes and abstypes

split off evaluation mechanisms in separte module Code_Eval

--HG--
rename : src/Tools/Code/code_ml.ML => src/Tools/Code/code_eval.ML

repaired broken code_const for term_of [String.literal]

modernized structure Theory_Target;

adding tracing function for evaluated code; annotated compilation in the predicate compiler

explicit indication of Unsynchronized.ref;

Code_Eval(uation)

--HG--
rename : src/HOL/Code_Eval.thy => src/HOL/Code_Evaluation.thy