export concl_of; induct method: admit "_";

tuned \isasymlbrace;

'insts' syntax; 'insert' method;

improved 'induct(_tac)' syntax;

added 'insert' method;

added inst, insts;

improved induct_tac;

induct stripped: match_tac;

Args.name_dummy;

fixed 'induct_tac' syntax;

handle dir prefix;

improved document preparation;

fixed comment;

added 'ML_command'; 'apply' etc.: comments;

apply etc.: comments;

tuned \isasymlbrace;

added \isasymlbrace, \isasymrbrace, \isasymtop;

'welcome' made diagnostic;

added Isar_examples/NestedDatatype.thy;

added NestedDatatype.thy;

added NestedDatatype;

fixed goal selection;

Isar: simplified (more robust) goal selection of proof methods; Isar: tuned 'let' syntax: replace 'as' keyword by 'and';

induct/case_tac emulation: optional rule; add_cases_induct: fixed case names;

HEADGOAL;

tuned comment;

removed "as" keyword;

suppress warning;

print_simpset / print_claset command;

case_tac / induct_tac: optional rule;

case_tac, induct_tac;

'let': replaced 'as' by 'and';

tuned recover;

isapar, isamarkuptext, isamarkuptxt turned into environments;

markup_env_command 'text' / 'txt';

support markup environments;

tuned presentation;

proper naming of fib equations;

recdef: admit names/atts;

isatool document: tuned -c option;

recdef: admit name and atts;

tuned -c option;

recover: observe stopper;

presentation ignore stuff: swallow newline;

added is_newline;

'cd': diag;

more robust handling of explicit rules;

tuned mixfix syntax;

added ProofGeneral.undo;

isatool document: check output file (workaround PolyML problem with RC);

use cong_add_global att;

added cong atts;

added cong atts;

made SML/XL happy;

change_global/local_css move to Provers/clasimp.ML; fixed 'iff' att syntax; added 'cong' att;

setup cong_attrib_setup;

added change_global/local_css;

added 'cong' att; fixed 'iff' syntax;

tuned;

params: preserve case names;

fixed indexing of elim rules;

use Attrib.add_del_args;

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];