use abstract code cerficates for bare code theorems

implement quotient_of for odl SML code generator

adjusted to cs. e4a7947e02b8

bound argument for abstype proposition

renamed theory Rational to Rat

tuned whitespace

more precise exception handler

more general case and induct rules; normalize and quotient_of; abstract code generation

crossproduct coprimality lemmas

lemma div_mult_swap, dvd_div_eq_mult, dvd_div_div_eq_mult

evaluation for abstypes

modernized structure Split_Rule; tuned signature; more antiquotations;

more antiquotations;

explicit @{type_syntax} markup;

explicit @{type_syntax} markup; misc tuning and simplification;

more orthogonal antiquotations for type constructors;

clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;

provide direct access to the different kinds of type declarations;

use mixfix syntax for Boogie types

merged

added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals

modernized syntax declarations, and make them actually work with authentic syntax;

observe standard convention for syntax consts;

proper type syntax (cf. 7425aece4ee3);

observe standard convention for syntax consts;

allow general mixfix syntax for type constructors;

merged

merged

remove redundant lemma realpow_increasing

remove redundant simp rules from RealPow.thy

adapt to new realpow rules

adapt to changes in simpset