proof markup: any mode;

replaced HOLogic.termTVar by HOLogic.termT;

ObtainFun;

METHOD_CLASET': refer to *local* claset;

moved obtain to obtain.ML;

TypeInfer.logicT; improved variable and pattern preparation;

tuned;

ObtainFun; prepare vars / asms / pats only once;

added thms_ctxt_args;

prepare patterns only once;

ObtainFun;

present chapter; tuned proof markup commands; moved obtain to obtain.ML;

removed pats;

chapter;

support for dummy variables (anyT, logicT); improved error msg: meet *before* assign;

TypeInfer.logicT;

new arg type for max_spec etc.

small changes;

removed inj_eq from the default simpset again

removed inj_eq from the default simpset again

removed inj_eq from the default simpset again

updated sml package name in installation exmaple

raw_t(e)xt: any proof mode;

fixed error msg;

marg_comment: repeat;

text: string list;

tidied, with a bit more progress

Working version after a FAILED attempt to base Follows upon LeadsETo

new weakening laws

removing the "{} : CC" requirement for leadsTo[CC]

back to old sml version (due to c library problems)

some tuning (incorporated David's suggestions)

working with weak LeadsTo in guarantees precondition\!

corrected, improved eMail addresses, user interface section

now workign as far as System_Alloc_Progress

SOUNDNESS BUG FIX for rotate_rule. The original code did not expect nested parameters such as !!y. Goal "!!x. x = a ==> (!!y. y ~= a ==> False)"; by (rotate_tac 1 1); be notE 1; ba 1; qed "foo"; val FalseI = standard (True_not_False RS (standard (refl RS foo)));

first working version to Alloc/System_Client_Progress; uses new "preserves" primitive instead of localTo

expandshort

dist page now in page/dist-{content|layout}

updated;

prettyfied

full url to local (munich) page

new web pages integrated

used for new weg page layout

ID line added

new webpage layout

abolition of localTo: instead "guarantees" has local vars as extra argument

used image_eq_UN to speed up slow proofs of base cases

useful lemma eqset_imp_iff

tuned;

tuned;

added Isar_examples/Fibonacci.thy;

Fixed bug in find-functions: list of parameters must be reversed before subsitution.

Renamed some vars

cosmetic mod.

accommodate current version of rpm;

Fixed a problem with returning from the last frame.

new generalized leads-to theory

fixed the discrepancy in the ordering of the constructors LESS EQUAL GREATER (for Moscow ML)

deleted rogue copy of localTo_imp_o_localTo

working version with new theory ELT

new theory UNITY/ELT

Goal: tuned pris;

Removed !!

Minimal.thy;

Isar_examples/Minimal.thy;

qed "";

Various little changes like cmethd -> method and cfield -> field.

del Method.ML

Minor mods.

renamed comp to compile (avoids clash with Relation.comp);

prove_goal thy;

Basis now Main.

tidied, choosing nicer names

distributive laws for * over -

tidied

new theorem rev_image_eqI

Added linord_less_split

re-shaped and re-ordered conversion relations

Streamlined it a bit more.

A small mod.

added Isar_examples/Puzzle.thy;

tidied

Streamlined it a bit.

removed full_SetCompr_eq from simpset() again

Added the proof by Nielson & Nielson.

tuned;

HOL changes

*** empty log message ***

Added MicroJava

*** empty log message ***

with_path;

Imported Conny's lemmas from MicroJava

clean target;

header;

tidied