various theorems about image and inverse image

Pi_empty1 is a more general simprule than empty_fun

rm -f *.aux;

simp_all method;

eliminated proof script;

HEADGOAL;

added prefer, defer;

added HEADGOAL;

added defer, prefer;

Drule.instantiate;

cp -r;

-p option;

added range_composition (also to simpset)

added finite_range_updI, finite_range_map_of, finite_range_map_of_override added, also to simpset: override_upd, ran_empty'

mkdir: prepare logic session directory;

added full_nat_induct

added splitE', also to claset

added inj_singleton

added finite_range_imageI

replaced FIRSTGOAL by FINDGOAL (backtracking!);

maintain standard rules (beware: classical provers provides another version!);

replaced FIRSTGOAL by FINDGOAL (backtracking!); improved flexflex handling; tuned sig;

tuned sig;

map data;

added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED

beautified spacing for binders with symbols syntax, analogous to HOL.thy

*** empty log message ***

'name' etc. include 'number'; attrib: include keyword_sid as name;

'name' syntax includes numbers;

optimized xs[i:=x]!j lemmas.

added map, map_st;

added map;

fallback on PureThy version;

replaced f : A funcset B by f``A <= B.

reflexivity simp rules

new theorem inj_on_restrict_eq

removed Isar_examples/Minimal;

fixed many bad line & page breaks

Documented Thm.instantiate (not normalizing) and Drule.instantiate (normalizing)

www;

Id line inserted

changes for the makepage script in Admin

makes Isabelle main web pages

Contents: suppress comments;

Thm.instantiate no longer normalizes, but Drule.instantiate does

still working; a bit of polishing

new lemmas for Ntree recursor example; more simprules; more lemmas borrowed from directory AC

change for new rewriting

added recursor

change in add_thmss to suppress warning

a bit of tidying

working version, with Alloc now working on the same state space as the whole system. Partial removal of ELT.

new theorem subset_Compl_self_eq

tuned comment;

Move some lemmas to List.

More lemmas.

isabellesimple: avoid paragraph;

int:nat->int is pushed inwards.

Forgot to "call" MicroJava in makefile. Added list_all2 to List.

tidied parentheses

tidied

new theorem leadsTo_refl and induction rule leadsTo_induct_pre

better automation for "slice"

moved some proofs from UNITY/ELT to UNITY/Project

obtain: renamed 'in' to 'where';

oops';

oops;

improved symbol for subcls relation

simplified definition of appl_methds, removing m_head

tuned;

obtain;

comment: any number of texts;

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;