isabelle update -u control_cartouches;

proper datatype for 8-bit characters

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

tuned -- avoid slightly odd @{cpat};

simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);

clarified context;

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

clarified signature;

explicit separation of signed and unsigned numerals using existing lexical categories num and xnum

tuned

--HG--
extra : rebase_source : f392005c56c1d890fea707e658b1e35131f31bf9

proper context for printing;

avoid (now superfluous) indirect passing of constant names

prefer explicit code symbol type over ad-hoc name mangling

eliminiated neg_numeral in favour of - (numeral _)

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

--HG--
extra : rebase_source : ff8027ac9606264aa4b2d4f8da037c426a3db98b

just one HOLogic.Trueprop_conv, with regular exception CTERM;
tuned;

prefer records with speaking labels over deeply nested tuples

--HG--
extra : rebase_source : 09acb7079a2d06a9c7f68aaaf04cedb0752142e0

merged fork with new numeral representation (see NEWS)

renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;

more coherent naming of syntax data structures

distinguish different classes of const syntax

code literals: distinguish numeral classes by different entries

allow individual printing of numerals during code serialization

more speaking function names for Code_Printer; added doublesemicolon

more antiquotations;

tuned whitespace

robustifed infrastructure for complex term syntax during code generation

explicit check for pattern discipline before code translation

code identifier namings are no longer imperative

fixed headers

back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;

distributed literal code generation out of central infrastructure

restructured code generation of literals

restructured and split code serializer module

New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1

fixed and tuned

explicit auxiliary function for code setup

joined theories IntDef, Numeral, IntArith to theory Int

simplified type int (eliminated IntInf.int, integer);

Logical operations on numerals (see also HOL/hologic.ML).