added coprimality lemma

tuned

tuned

more canonical name (2)

more canonical name

added lemma

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

all headings in upper case

more int/nat transfer rules; examples of new untransferred attribute

more transfer rules for sets

implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction

use right context when exporting variables (cf. AFP Coinductive_List failures)

keep track of nested BNFs

tuning

implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>

SPASS has more Uppercase keywords than I was fearing -- better always append _

merge

tuning

adapted example (cf. 78a3d5006cf1)

code simplifications (cf. 78a3d5006cf1)

killed dead code

changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1

killed dead code

tuning

tuning

tuning

tuning

tuning

tuning

tuning

tuning

tuning

tuning

tuning

tuning

tuned

tuned variable names

tuned

tuning

tuning

[mq]: tuning

tuning

tuning

tuning

tuning

fixed failure in coinduction rule tactic

too much qualification is like too little

tuning

tuning

tuning

merge

tuning

tuned defs

avoid duplicate call to "mk_fold_rec_args_types" function

continuation of f461dca57c66

renamed ML variables

tuned record field names to avoid confusion between low-level and high-level constants/theorems

tuned signature

support induction principles with multiple occurrences of the same type in "fpTs" and (hopefully) with loss of recursion (e.g. primrec definition of is_nil, where the IH can be dropped)

tuned ML variable names

transfer rule for listsum

more reflexivity rules (for OO)

tuning

avoid code duplication

eliminated dead argument

one less flaky "fpTs" check (flaky in the presence of duplicates in "fpTs", which we want to have in "primrec")

tuning

simpler, more robust iterator goal construction code

tuning

reverted 23929f647f79 -- not needed after all

killed dead code

tuning

slightly nicer ML interface

added convenience function

keep a record of the fixpoint equations

export ML function (needed for "primrec_new")

export ML function

corrected name

tuned proofs

type class for confined subtraction

denesting of functions

some meagure hints concerning reification

make reification part of HOL

permissive uncheck -- allow printing of malformed terms (e.g. in error messages);

Type_Annotation only works *after* uncheck (which usually requires authentic type information);

updated isatest stats;

tuned theory name

tuned rules

tuning

renamed util function

tuned;