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;