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

new-style infix declaration for "image"

Fixed obsolete use of "op ^^"; new lemma

tuned;

tidied

new psubset lemma

added foldr

Algebra and Polynomial theories, by Clemens Ballarin

Algebra and Polynomial theories, by Clemens Ballarin

tuned;

MUCKE_HOME;

Id;

improved;

tuned;

RPMRELEASE;

inserted {...}

updated;

updated;

tuned;

tuned;

Isabelle99;

fixed deps;

tuned;

tuned;

improved presentation;

tuned;

isabellesym.sty;

definitions of many Isabelle symbols;

final update by Gertrud Bauer;

workaround bug (feature?) in bibtex;

tuned;

comment out isabellesym.sty;

improved;

\isasymbol renamed to \isasym;

tuned;

tuned msg;

\isasym;

improved singleton_insert_inj_eq

improved presentation;

fixed deps;

tuned;

expandshort; tidied

localTo_imp_o_localTo is now really an implication

simplified the stable_completion proofs

tidied

expandshort

improved IsarThy.init_context;

tuned;

added various little lemmas

clarsimp_tac now copes with the (unwanted) case that the simplifier splits the goal

tuned msg;

tuned;

added (try_)update_thy_only; added (try_)context_thy_only command;

added init_context;

quiet_update_thy: ml flag; replaced broken del_deps by upd_deps; begin_theory: better handling of 'files';

Fixed a bug in the EX simproc.

export cond_with_path;

dummy_pattern: aprop;

updated for Isabelle99;