adjust layout for book

merged

Added continuity and determinism proof

Added parantheses to code_type for heap monad

improved defs and proofs

use \<^isub> in determ proof for display in book

merged

export dom predicate in the info record

export cases rule in the info record

made proofs more readable

pragmatic executability for instance real :: open

lifting for primitive definitions; explicit conversions from and to lists of coefficients, used for generated code; replaced recursion operator poly_rec by fold_coeffs, preferring function definitions for non-trivial recursions; prefer pre-existing gcd operation for gcd

selection operator smallest_prime_beyond

documentation on code_printing and code_identifier

more consistent parsing and reading of classes and type constructors

another example lemma

store more theorems in data structure

tuning

simplified proofs

prefer xsymbol for book

same order of properties as in While rule

some comments on syntax and automation setup

uncheck terms before annotation to avoid awkward syntax

tuning

tuning

make use of show_type_emphasis instead of using hack; make sure global configurations don't affect proof script creation

reflexive nbe equation for equality on String.literal

tuned whitespace

dropped relics of ancient binary numeral case study

merged