actually use Data.sizef, not hardwired size_of_thm;

more scalable PARALLEL_GOALS, using more elementary retrofit; tuned signature;

tuned

merged

less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context; even less intrusive PREFER_GOAL (without structural goal marker), e.g. relevant for generic_simp_tac; adapted ZF proof that broke for unknown reasons (potentially slight change of Drule.size_of_thm);

SOMEthing went utterly wrong;

tuned signature;

more position information for markup;

tuned: cleaned up data structure

simplified data structure

ommit trivial tfrees in annotations

Generalize trace_mult_sym to square products of non-square matrices.

prefer Safari for viewing PDF files, which appears to be better behaved than Preview concerning re-opening recent files (Mountain Lion);

recover command tags from 4cf3f6153eb8 -- important for document preparation;

clarified ISABELLE_DOC_FORMAT -- eliminated slightly odd fall-back;

more robust Doc.view invocation: avoid executing process on GUI thread, but show errors as dialog;

more robust options, notably for isatest mac-poly-M8-skip_proofs;

dockable window for Isabelle documentation;

slightly improved "isabelle doc" based on Isabelle/Scala; updated documentation of "isabelle display";

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

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;

make SML/NJ partially happy;

reflection without evaluation

decomposed reflection steps into conversions; deholified reification procedure; prefer Subgoal.FOCUS over SUBGOAL

permit multiple variable arguments in reflect

tuned

dropped vacuous prefix

combinator fold_range, corresponding to map_range

merged

more VC -> VCG

VCG is standard name

used nice syntax, removed lemma because it makes a nice exercise.

NEWS about Spec_Check

tuned headers;

tuned messages -- some attempts to observe Isabelle output channel semantics;

less verbosity -- do not print final ();

tuned -- dynamic ML context is updated incrementally (see also e7c47fe56fbd);

tuned;

toplevel invocation via implicit ML compilation context;

more direct Context.setmp_thread_data for one-way passing of context;

tuned;

tuned;

do not open ML structures;

prefer separate 'ML_command' for parallel evaluation;

simplified context and data management -- plain ctxt: Proof.context is default for most operations;

more conventional spelling and grammar;

minor tuning -- more linebreaks;

removed pointless comment -- NB: Isabelle output is message-oriented with implicit line-boundaries;

standardized aliases;

do not handle arbitrary exceptions;

added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;

merged

tuned signature;

tuned signature; tuned;

misc tuning;

prefer existing beta_eta_conversion;

more standard fold/fold_rev;

tuned import;

misc tuning;

prefer existing beta_eta_conversion;

more standard names;

simplified method setup;

tuned -- prefer terminology of tactic / goal state;

tuned;

misc tuning;

tuned;

tuned signature;

stay within regular tactic language -- avoid operating on whole proof state;

standardized aliases;

space between minus sign and number for large negative number literals causes NumberFormatException at run-time

tuned

relational version of HoareT

obsolete;

resolve_inc_tyvars: back to old behavior before 0fa3b456a267 where types of equal Vars are *not* unified -- recover last example in src/HOL/Metis_Examples/Clausification.thy;

more precise "incremented" indication, which might be relevant in corner cases, e.g. instantiation of leading to vars with different types (which is a potential problem nonetheless);

tuned signature -- more explicit flags for low-level Thm.bicompose;