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;

method setup;

tuned comments;

'prop', 'term', 'typ';

load;

export exn_message;

removed trace;

BREAK: include state; report Attrib.ATTRIB_FAIL, Method.METHOD_FAIL;

have_tthms; assume: store actual asms;

PureThy.default_name; have_tthms;

generalized (opt_)thm_name; xthm, xthms1;

exception METHOD_FAIL;

added have_theorems, have_lemmas, have_facts; tuned from_facts; Theory.apply replaced by Library.apply;

added 'theorems', 'lemmas', 'note'; tuned 'thm';

break: exhibit state; removed print_thm;

exception ATTRIB_FAIL; local_attribute'; removed 'lemma', 'assumption'; added 'where', 'with';

removed trace;

Symbol.space;

space;

val spc: int -> T;

added default_name; added have_tthmss;

Drule.rev_triv_goal;

Theory.apply replaced by Library.apply;

val apply: ('a -> 'a) list -> 'a -> 'a; val transform_failure: (exn -> exn) -> ('a -> 'b) -> 'a -> 'b;

export vars_of and friends; open BasicDrule only;

Pretty.spc;

added pretty_tthms, print_tthms; tuned apply(s);

new theory UNITY/PPROD

new theory PPROD

a faster proof

removed genelim.ML;

thm, thms;

added print_thm;

made SML/NJ happy;

added oo, ooo (*concatenation: 2 and 3 args*);

Attribute.tthms_of; Theory.copy;

Attribute.tthms_of;

Attribute.thms_of;

Classical.setup, attrib_setup;

attrib_setup: rulify;

attrib_setup;

all modifiers turned into attributes; realistic method syntax; smart_simp method;

tuned attribute names; all modifiers turned into attributes; realistic method syntax;

several args parsers; realistic syntax; tuned;

tuned names;

renamed tac / etac to refine / then_refine;

add print_theorems; print_thms: handle attributes; renamed tac / etac to refine / then_refine; tuned comments; load arg: name;

add print_theorems; print_thms: handle attributes;

several args parsers; realistic syntax; attributes: transfer, RS, APP, where, standard, elimify;

several args parsers; include positions; misc tuning;

removed args, args1, thm_xname; fixed nat: Symbol.explode; name / xname: include sym_ident; keyword_symid: include ident; tuned atom_arg; support nested args;

replaced is_symid by is_sid;

renamed init_context to init;

renamed init_context to init; added read_termTs; added declare_thm;

structure PureIsar;

removed lift_modifier; removed fail; added tthms_of; added print_tthm; tuned rule;

Attribute.thms_of;

Scan.read;

added read;

tuned usage of read;

generalized JN_empty and added reachable_SKIP

removed the reference to mesontest2.ML, itself now deleted

moved some facts about Pi from ex/PiSets to Fun.ML

prefixed op;

Theory.copy;

val copy: theory -> theory;

added unless, first;

added read_nat;

not needed in distribution

needed tidying desperately

qualified the name "restrict" since Fun.restrict exists too

moved Pi and -> (renamed funcset) to Fun.thy

the type of @evalcn was wrong

moved UNION_o to Fun.ML, since Fun.thy is no longer a parent of equalities

no longer loads Fun so that the Fun proofs can use equalities.thy

the function space operator

New section on advanced datatypes.

*** empty log message ***

mesontest2.ML was never needed in the distribution

changed inverse syntax from x-| to i(x)

proved surjI

tidied

Big simplification of proofs. Deleted lots of unnecessary theorems

tiny changes;

changed to a link;

local simpset theory data; simp add / del attributes; smart_simp_tac and method;

local claset theory data; intro, elim, dest, del attributes; single_tac and method; fast, best etc. methods;

Object logic specific operations.

Isar setups;

added metacuts_tac;

removed local_theory;