more frugal simp rules for bit operations; more pervasive use of bit selector

--HG--
extra : rebase_source : 09f56fd30f4ab8ae84811041575772264eb330b3

rule concerning bit (push_bit ...)

more specific class assumptions

tuned material

--HG--
extra : rebase_source : 28017ca9e3c54a758db0e8c3ac45e1c2b31b6f65

characterization of singleton bit operation

strengthened type class for bit operations

bit shifts as class operations

tuned syntax

slightly more specialized name for type class

irrelevant

--HG--
extra : rebase_source : fff50fd15be0f5d17aa176677f7d646cc5e44265

"export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports;
"export_code ... file" is legacy, the empty name form has been discontinued;
updated examples;

improved code equations taken over from AFP

migrated from Nums to Zarith as library for OCaml integer arithmetic

--HG--
extra : rebase_source : 9da06716fa2cece20a04b2b74f042738c493e925

isabelle update -u control_cartouches;

proper datatype for 8-bit characters

algebraic embeddings for bit operations

generalized

ran isabelle update_op on all sources

kill old size infrastructure

added lemmas and tuned proofs

--HG--
extra : rebase_source : 96f42feb3c60e71f2655c97d331ac68baf8b4a63

clarified parity

--HG--
extra : rebase_source : 7e46e7dfc0f09316c589babeb5a372aeff091071

clarified uniqueness criterion for euclidean rings

--HG--
extra : rebase_source : 3f8d28b5e69282e9e5f36f72ad0d4d2e551ca7ab

tuned imports

--HG--
extra : rebase_source : bc9797cb892085195c2d8662a7ca3896dd1e5011

euclidean rings need no normalization

--HG--
extra : rebase_source : 7f2e3f676b513d6c59f526f099be30240183bf05

one uniform type class for parity structures

--HG--
extra : rebase_source : edf12af006cee8d114754f4a1916094166004337

abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel

--HG--
extra : rebase_source : c6612d6016d811043143eafb7a671631287494a1

avoid fact name clashes

--HG--
extra : rebase_source : dadb340e6deb1d95749a6828999b5295bffc7702

more direct construction of integer_of_num;
code equations for integer_of_char may rely on pattern matching on Char

--HG--
extra : rebase_source : 40a2196ad040f66707469d6b3d1be2b7a4b1dc68

computation preprocessing rules to allow literals as input for computations

slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization

--HG--
extra : rebase_source : 0d5af77e2a7d66625c22923a19c456b1ca17652e

more fine-grained type class hierarchy for div and mod

--HG--
extra : rebase_source : fffbeef99e834ca17596f478178e94bed8a014bc

eliminated irregular aliasses

transfer rules for divides relation on integer and natural

transfer lifting rule for numeral

--HG--
extra : rebase_source : bafc2cb3fd6a49a365472e2fb15a4de692ec874d

syntactic type class for operation mod named after mod;
simplified assumptions of type class semiring_div

--HG--
extra : rebase_source : 3714be7474835787b2a513b731c9864d1ac9d2c4

do not export abstract constructors in code_reflect

add serialisation for abs on integer to target language operation

monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime

--HG--
extra : rebase_source : e05d79a48b81d6ffe67aca3743dbab1781bd1e4f

more selective preprocessing allows bare "numeral" occurences to be retained as real function in generated code

--HG--
extra : rebase_source : ac120f7c610071f077b4f216c87e32c562d227fc

eliminated \<Colon>;

direct bootstrap of integer division from natural division

isabelle update_cartouches;

Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.

separate class for division operator, with particular syntax added in more specific classes

distributivity of partial minus establishes desired properties of dvd in semirings

--HG--
extra : rebase_source : 99dad957de0410b3a1ca21ff1f8723495b31194f

default abstypes and default abstract equations make technical (no_code) annotation superfluous

--HG--
extra : rebase_source : d54bb7382702f44984b3e0e4b39bf01c86d63963

modernized header uniformly as section;

always annotate potentially polymorphic Haskell numerals

--HG--
extra : rebase_source : afdd470c78d704a706fe6d34761f4251b2b79ec0

tuned

--HG--
extra : rebase_source : f392005c56c1d890fea707e658b1e35131f31bf9

keep obsolete interpretations in Main, to avoid merge trouble

reintroduced an instantiation of 'size' for 'numerals'

moved old 'size' generator together with 'old_datatype'

--HG--
rename : src/HOL/Tools/Function/old_size.ML => src/HOL/Tools/Old_Datatype/old_size.ML

renamed 'rep_datatype' to 'old_rep_datatype' (HOL)

reduced name variants for assoc and commute on plus and mult

renamed 'xxx_size' to 'size_xxx' for old datatype package

renamed 'fun_rel' to 'rel_fun'

unregister lifting setup following the best practice of Lifting

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

make integer_of_char and char_of_integer work with NBE and code_simp

adapted theories to 'xxx_case' to 'case_xxx'
* * *
'char_case' -> 'case_char' and same for 'rec'
* * *
compile
* * *
renamed 'xxx_case' to 'case_xxx'

renamed '{prod,sum,bool,unit}_case' to 'case_...'

eliminiated neg_numeral in favour of - (numeral _)

execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs

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

--HG--
extra : rebase_source : ff8027ac9606264aa4b2d4f8da037c426a3db98b

patch Isabelle ditribution to conform to changes regarding the parametricity

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

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

discontinued obsolete typedef (open) syntax;

restrict unqualified imports from Haskell Prelude to a small set of fundamental operations

removed Nat_Numeral.thy, moving all theorems elsewhere

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

use qualified constant names instead of suffixes (from Florian Haftmann)

attribute code_abbrev superseedes code_unfold_post

--HG--
extra : rebase_source : c121dde677a8fb25289c668f8f6a123174fb117d

prefer typedef without extra definition and alternative name;
tuned proofs;

avoid using legacy theorem names

use module integer for Eval

Haskell == is infix, not infixl

renamed class/constant eq to equal; tuned some instantiations

another refinement chapter in the neverending numeral story

avoid unreliable Haskell Int type

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

adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler

tuned whitespace

more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS

code literals: distinguish numeral classes by different entries

allow individual printing of numerals during code serialization

some syntax setup for Scala

Adapted to changes in induct method.

moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly

moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly

moved theory Divides after theory Nat_Numeral; tuned some proof texts

prefer code_inline over code_unfold; use code_unfold_post where appropriate

code attributes use common underscore convention

OCaml builtin intergers are elusive; avoid

added lemma about 0 - 1

String.literal replaces message_string, code_numeral replaces (code_)index

--HG--
rename : src/HOL/Code_Index.thy => src/HOL/Code_Numeral.thy