more formal isabelle_admin_build; tuned;

misc tuning and clarification;

need to run isabelle update_keywords, but not to check it (cf. 4cf3f6153eb8);

obsolete -- cf. isabelle.Keywords in Scala;

improved "isabelle keywords" and "isabelle update_keywords" based on Isabelle/Scala, without requiring to build sessions first; tuned signature;

back to keyword 'pr' :: diag as required for ProofGeneral command line -- reject this TTY command in Isabelle/jEdit by other means;

more formal ProofGeneral command setup within theory Pure; consider 'ProofGeneral.pr' as control command as well;

tuned;

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

more appropriate cutting of input syntax

tuned variable names

tuned message -- more markup;

tuned message;

proper diagnostic command 'print_state';

detach process more reliably -- NB: viewer might be synchronous or asynchronous depending on settings;

clones of increase-font-size / decrease-font-size to allow two further shortcuts for various keyboard layouts;

Scala version of "isabelle doc"; discontinued slightly odd / unused ">>" comments within Contents (see also b077b79061b6);

ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);

actually observe print_depth for outer term structure;

support for XML data representation of proof terms;

updated to scala-2.10.2;

tuned;

clarified strings of symbols, including ML string literals;

more on managed evaluation;

more on managed evaluation;

updated to Isabelle2013;

tuned;

tuned;

eliminated old "ref" manual;

more on built-in syntax transformations, based on reduced version of old material;

misc tuning and clarification;

more on concrete syntax of proof terms;

more on reconstructing and checking proof terms;

more examples on proof terms;

obsolete;

updated operations on proof terms;

more on proof terms;

updated documentation of sort hypotheses;

Explain to beginners why Complex_Main

more set theory

Code_Real_Approx_By_Float: remove code equations using Ratreal

tuned

added lemma

tuned theory name

tuned

added lemma

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