the + facility for locales, by Florian

new Close_locale synatx

towards handling sharing of variables

tidying

expandshort

better export for nested locales

new (and generalized) theorems about Sigma/Times

locales: assumes and defines may be empty

locales

and_list;

Addition of the States component; parts of Comp not working

tuned;

IOA-Storage: Memory storage case study.

Memory storage case study.

Memory storage case study from PhD p.240;

new theorem Pow_UNIV

new rule rev_bexI

new theorems Domain_Union, Range_Union

removed duplicate contrapos;

enum: !!! after seperator;

excursion: ERROR_MESSAGE; exn_message: ERROR;

qed: kind_name (again);

show_tags flag;

new theorem INT_Un

better version of Image_diag

tactical CHANGED now uses alpha-eta conversion, not alpha conversion Streamlined code

Renamed subset_Sigma_llist to subset_Times_llist

new theorems about diag

fixed declatation of patterns and skolem;

tuned print_state; changed solve semantics: support back-pressure of asms (cut, def etc.);

tuned welcome msg;

added restart;

added exception RESTART;

proof_general_trans (experimental);

replaced wakeup by decorate_prompt_fn;

eliminated "Trying to recover ..." msg;

added oct_char;

method brute_force = ALLGOALS force_tac;

*** empty log message ***

At last: linear arithmetic for nat!

Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.

fixed a link

added Real/Hyperreal

Addition of Hyperreal theories Zorn and Filter

moved diag (diagonal relation) from Univ to Relation

tidied up list definitions, using type 'a option instead of unit + 'a, also using real typedefs instead of faking them with extra rules

tuning to assimiliate it with PhD;

Added a general refutation tactic which works by putting things into nnf first.

Added filter_prems_tac

removed prs / prs_fn;

guarantees laws

simplified ensures_UNIV

new thms for invariant

new theorem program_equalityE

renamed vars

image_id in simpset

removed prs / prs_fn (broken, because it did not include \n in its semantics, forcing writeln to add one uncoditionally); replaced prs_fn by writeln fn;

eliminated ISABELLE_INTERFACE_OPTIONS;

improved comment; removed ISABELLE_INTERFACE_OPTIONS; added ProofGeneral;

replaced prs by std_output;

replaced prs by writeln;

replaced prs by std_output / writeln;

comment parser;

add_text, add_chapter etc.: dummy;

chapter etc. headings; use, use_thy, cd: name;

tuned space;

replaced prs by writeln;

removed redirect_to_latex stuff;

Isar.main();

setup Blast.setup; setup Clasimp.setup;

added commands;

added isar.ML;

Isabelle/Isar main interface.

fixed prefix_lines: *separate* by \n;

added Isar/isar.ML;

fixed links

print_state hook, obeys Goals.current_goals_markers by default;

print_state: use begin_goal from Goals.current_goals_markers;

added undos, redos;

tty: issue wakeup;

std_output, prefix_lines;

better miniscoping rules: the premise C~={} is not good because Safe_tac eliminates such assumptions.

fixed method syntax;

break: exhibit state stack;

match_bind: 'as' patterns; statements: 'is' patterns;

let: 'as' patterns; statements: propp ('is' patterns);

match_bind(_i): 'as' patterns; assume, theorem, show etc.: propp; tuned qed msg;

term_pat vs. prop_pat; added bind_propp(_i); assume: propp;

term_pat vs. prop_pat;

no warning for "it" theorems;

tidied

Finally removing "Compl" from HOL

exn_message FAIL;

blast: cla_method';

export simp_modifiers;

expoer cla_method('), cla_modifiers;