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

--HG--
extra : rebase_source : 09f56fd30f4ab8ae84811041575772264eb330b3

bit shifts as class operations

slightly more specialized name for type class

migrated from Nums to Zarith as library for OCaml integer arithmetic

--HG--
extra : rebase_source : 9da06716fa2cece20a04b2b74f042738c493e925

proper code_simp setup for literals

--HG--
extra : rebase_source : 419d15d6c51642cd5dc03c383eff3a88eda5f90b

prefer proper strings in OCaml

isabelle update -u path_cartouches;

isabelle update -u control_cartouches;

isabelle update_cartouches -t;

prefer HTTPS;

uniform tagging for printable and non-printable literals

proper datatype for 8-bit characters

new lemma

dedicated append function for string literals

ran isabelle update_op on all sources

more symbols;

lifting setup for char

--HG--
extra : rebase_source : bb7bcf88b2f19b193b28620c0e9a2bb78e69feb4

proper concept of code declaration wrt. atomicity and Isar declarations

--HG--
extra : rebase_source : adb08da85e01b6c9c81d471a0d8e7ebb68d7e472

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

emphasize dedicated rewrite rules for congruences

--HG--
extra : rebase_source : 28c5807c3eda548e5ed0637459d63997c46e3ff3

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

--HG--
extra : rebase_source : 3714be7474835787b2a513b731c9864d1ac9d2c4

unified CHAR with CHR syntax

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

moved

more direct bootstrap of char type, still retaining the nibble representation for syntax

--HG--
extra : rebase_source : fd206c5addb099b720d632a7511e1485f7f64874

isabelle update_cartouches -c -t;

disable generation of 'case_transfer' for 'nibble', due to quadratic proof -- to make 'HOL-Proofs' happier

eliminated \<Colon>;

standardized some occurences of ancient "split" alias

--HG--
extra : rebase_source : 706ba501d5c0596a2bde6e46d42aa8464a91ede5

tuned signature;

isabelle update_cartouches;

clarified context;

Thm.cterm_of and Thm.ctyp_of operate on local context;

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

explicit type annotation avoids problems with Haskell type inference

modernized header uniformly as section;

modernized setup;

updated news

use 'datatype_new' in 'Main'

reduced name variants for assoc and commute on plus and mult

qualified String.explode and String.implode

added [simp]

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

use balanced tuples in 'primcorec'

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

make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals

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

added \<newline> symbol, which is used for char/string literals in HOL;

setup lifting/transfer for String.literal

add congruence rule to prevent code_simp from looping

abort execution of generated code with explicit exception message

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

--HG--
extra : rebase_source : ff8027ac9606264aa4b2d4f8da037c426a3db98b

reflexive nbe equation for equality on String.literal

simplifier uses proper Proof.context instead of historic type simpset;

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

--HG--
extra : rebase_source : 982810ecce9e31070e2293715ed744c3b68ae21d

incorporated constant chars into instantiation proof for enum;
tuned proofs for properties on enum of chars;
swapped theory dependency of Enum.thy and String.thy

moved quite generic material from theory Enum to more appropriate places

--HG--
extra : rebase_source : aada8b3ff46b715201e6ecbb53f390c25461ebd9

discontinued obsolete typedef (open) syntax;

prefer ML_file over old uses;

renamed "xstr" to "str_token";

inner syntax positions for string literals;

removing old code generator setup for strings

observe distinction between sets and predicates more properly

discontinuend obsolete Thm.definitionK, which was hardly ever well-defined;

eliminated Codegen.mode in favour of explicit argument;

renewing specifications in HOL: replacing types by type_synonym

reverted cs. 0a3fa8fbcdc5 -- motivation is unreconstructable, produces confusion in user space

renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;

--HG--
rename : src/Pure/pure_thy.ML => src/Pure/global_theory.ML

renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI

fiddling with the correct setup for String.literal

Haskell == is infix, not infixl

changing String.literal to a type instead of a datatype

expand_fun_eq -> ext_iff
expand_set_eq -> set_ext_iff
Naming in line now with multisets

renamed class/constant eq to equal; tuned some instantiations

more antiquotations;

tuned module names

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

modernized structures;

modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;

some syntax setup for Scala

tuned

map_range (and map_index) combinator

prefer code_inline over code_unfold; use code_unfold_post where appropriate

code attributes use common underscore convention

constant "chars" of all characters

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

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

is a definition

added new kind generated_theorem for theorems which are generated by packages to distinguish between theorems from users and packages

proper structures for list and string code generation stuff

refined HOL string theories and corresponding ML fragments

moved into Main;

improved string syntax (allow translation rules);

Tools/string_syntax.ML;

'a list: Nil, Cons;

xstr token class;

moved String theory to main HOL;