added add_del_args;

fixed goal syntax;

comments modified

tuned

included new stanford mirror, mirror links now point to source directly

updated recdef

tuned;

recdef

If all termination conditions are proved automatically, the recusrion equations are added to the simpset automatically. recdef.rules -> recdef.simps

recdef.rules -> recdef.simps

mod in recdef allows to access the correct simpset via simpset().

the simplification rules returned from TFL are now paired with the row they came from.

* Isar/Pure: local results and corresponding term bindings are now subject to Hindley-Milner polymorphism (similar to ML); this accommodates incremental type-inference nicely; * Isar/Pure: new calculational elements 'moreover' and 'ultimately' support plain accumulation of results, without applying any rules yet;

support Hindley-Milner polymorphisms in results and bindings;

added 'moreover' and 'ultimately';

added \MOREOVER, \ULTIMATELY;

support Hindley-Milner polymorphisms in binds and facts; let_bind(_i): polymorphic version; moved find_free, export_wrt to Isar/proof_context.ML;

support Hindley-Milner polymorphisms in binds and facts; let_bind(_i): polymorphic version; improved warn_extra_tfrees; added find_free, export_wrt (from Isar/proof.ML);

let_bind(_i): polymorphic version;

ProofContext.find_free;

'tactic': refer to PureIsar structure;

?this: support params;

support polymorphic Vars;

tuned;

foldl_term_types: depend on term as well;

read_def_cterms: use Sign.read_def_terms;

read_def_terms (no certify yet);

export update_multi;

added tvars_intr_list;

*** empty log message ***

*** empty log message ***

mods because of weak_case_cong -> removed Action.ML twice

added weak_case_cong feature

mods because of weak_case_cong

fixed railqtoken;

-I option;

renamed 'hoare_vcg' to 'hoare';

tuned;

fixed dddot_tr;

rail token vs. terminal;

fixed term syntax;

tail token vs. terminal;

fixed \rail@tokenfont (ever used?);

added an order-sorted version of quickSort

simplified constant "colored"

added 'ultimately';

added WhileRule'; tuned;

made SML/NJ happy;

tuned presentation;

tuned;

ignore_stuff; P.!!!!;

tuned output;

!!!! = cut "Corrupted outer syntax in presentation";

added is_begin/end_ignore;

tuned targets;

tuned;

improved (anti)quote_tr(');

addsimprocs [record_simproc];

tuned antiquote_tr';

export updateN;

use abstract syntax; 'hoare' method;

plain ASCII;

arith method: HEADGOAL;

HOL/ex/Multiquote;

added HOL/ex/Multiquote.thy;

tuned;

usedir -D: update styles as well;

usedir -D: update styles;

improved dump of styles;

-o sty;

comments

added 'moreover' command;

tuned output;

tuned spacing;

ex/Antiquote.thy made new-style theory; removed ex/Antiquote.ML;

now exclusively uses rtac/dtac/etac rather than the long forms

restored the MESON examples file HOL/ex/mesontest2.ML

made a proof more robust (did not like Suc_less_eq)

Suc_less_eq now with AddIffs. How could this have been overlooked?

combined finite_Int1/2 as finite_Int. Deleted the awful "lemma" from the default claset. Used "inst"

made more robust

tidied using new "inst" rule

tidied using new "inst" rule

new meta-rule "inst", a shorthand for read_instantiate_sg

goal_spec: [!];

tuned;

tuned;

tuned;

tuned comment;

help message;

handle general case: params and hyps of thesis;

soft_asm_tac: hack to norm goal;

proof methods: 'case_tac' / 'induct_tac';

tuned degenerate cases / induct;

added prove_goalw_cterm; quick_and_dirty moved here;

quick_and_dirty moved to Isar/skip_proof.ML;

use Args.goal_spec; added subgoal_tac;

goal_spec;

ALLGOALS_RANGE superceded by Seq.INTERVAL;

improved support for emulating tactic scripts;

res_inst_tac etc.; subgoal_tac;

goalspec;

case_tac, induct_tac;

tactic emulation;

tidied

the perm_rules variable is no longer needed

tidied

replaced best_tac by force_tac, allowing some arithmetic reasoning

renamed a variable to avoid possible free/bound confusion

a possibly (?) more perspicous simprule in the "simpset" part

now based on "Main", as it should be

deleted unnecessary "simpset" part from recdef

'oops' made proper; removed 'kill_proof' (superceded by 'kill');

intro_classes_tac: REPEAT_ALL_NEW;

tuned comments;

tuned;

obtain; moved pure methods / atts to pure.tex; tuned;

simplified setup; tuned;

pure methods / atts moved here; tactic emulation moved here; oops moved here; history commands; tuned;

tuned;