2000-04-01 wenzelm 2000-04-01 recdef: admit names/atts;
2000-04-01 wenzelm 2000-04-01 isatool document: tuned -c option;
2000-04-01 wenzelm 2000-04-01 recdef: admit name and atts;
2000-04-01 wenzelm 2000-04-01 tuned -c option;
2000-04-01 wenzelm 2000-04-01 recover: observe stopper;
2000-04-01 wenzelm 2000-04-01 presentation ignore stuff: swallow newline;
2000-04-01 wenzelm 2000-04-01 added is_newline;
2000-04-01 wenzelm 2000-04-01 'cd': diag;
2000-04-01 wenzelm 2000-04-01 more robust handling of explicit rules;
2000-04-01 wenzelm 2000-04-01 tuned mixfix syntax;
2000-04-01 wenzelm 2000-04-01 added ProofGeneral.undo;
2000-04-01 wenzelm 2000-04-01 isatool document: check output file (workaround PolyML problem with RC);
2000-03-31 wenzelm 2000-03-31 use cong_add_global att;
2000-03-31 wenzelm 2000-03-31 added cong atts;
2000-03-31 wenzelm 2000-03-31 added cong atts;
2000-03-31 wenzelm 2000-03-31 made SML/XL happy;
2000-03-31 wenzelm 2000-03-31 change_global/local_css move to Provers/clasimp.ML; fixed 'iff' att syntax; added 'cong' att;
2000-03-31 wenzelm 2000-03-31 setup cong_attrib_setup;
2000-03-31 wenzelm 2000-03-31 added change_global/local_css;
2000-03-31 wenzelm 2000-03-31 added 'cong' att; fixed 'iff' syntax;
2000-03-31 wenzelm 2000-03-31 tuned;
2000-03-31 wenzelm 2000-03-31 params: preserve case names;
2000-03-31 wenzelm 2000-03-31 fixed indexing of elim rules;
2000-03-31 wenzelm 2000-03-31 use Attrib.add_del_args;
2000-03-31 wenzelm 2000-03-31 added add_del_args;
2000-03-31 wenzelm 2000-03-31 fixed goal syntax;
2000-03-31 nipkow 2000-03-31 comments modified
2000-03-31 kleing 2000-03-31 tuned
2000-03-31 kleing 2000-03-31 included new stanford mirror, mirror links now point to source directly
2000-03-31 nipkow 2000-03-31 updated recdef
2000-03-30 wenzelm 2000-03-30 tuned;
2000-03-30 nipkow 2000-03-30 recdef
2000-03-30 nipkow 2000-03-30 If all termination conditions are proved automatically, the recusrion equations are added to the simpset automatically. recdef.rules -> recdef.simps
2000-03-30 nipkow 2000-03-30 recdef.rules -> recdef.simps
2000-03-30 nipkow 2000-03-30 mod in recdef allows to access the correct simpset via simpset().
2000-03-30 nipkow 2000-03-30 the simplification rules returned from TFL are now paired with the row they came from.
2000-03-30 wenzelm 2000-03-30 * 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;
2000-03-30 wenzelm 2000-03-30 support Hindley-Milner polymorphisms in results and bindings;
2000-03-30 wenzelm 2000-03-30 added 'moreover' and 'ultimately';
2000-03-30 wenzelm 2000-03-30 added \MOREOVER, \ULTIMATELY;
2000-03-30 wenzelm 2000-03-30 support Hindley-Milner polymorphisms in binds and facts; let_bind(_i): polymorphic version; moved find_free, export_wrt to Isar/proof_context.ML;
2000-03-30 wenzelm 2000-03-30 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);
2000-03-30 wenzelm 2000-03-30 let_bind(_i): polymorphic version;
2000-03-30 wenzelm 2000-03-30 ProofContext.find_free;
2000-03-30 wenzelm 2000-03-30 'tactic': refer to PureIsar structure;
2000-03-30 wenzelm 2000-03-30 ?this: support params;
2000-03-30 wenzelm 2000-03-30 support polymorphic Vars;
2000-03-30 wenzelm 2000-03-30 tuned;
2000-03-30 wenzelm 2000-03-30 foldl_term_types: depend on term as well;
2000-03-30 wenzelm 2000-03-30 read_def_cterms: use Sign.read_def_terms;
2000-03-30 wenzelm 2000-03-30 read_def_terms (no certify yet);
2000-03-30 wenzelm 2000-03-30 export update_multi;
2000-03-30 wenzelm 2000-03-30 added tvars_intr_list;
2000-03-29 nipkow 2000-03-29 *** empty log message ***
2000-03-29 nipkow 2000-03-29 *** empty log message ***
2000-03-28 nipkow 2000-03-28 mods because of weak_case_cong -> removed Action.ML twice
2000-03-28 nipkow 2000-03-28 added weak_case_cong feature
2000-03-28 nipkow 2000-03-28 mods because of weak_case_cong
2000-03-28 wenzelm 2000-03-28 fixed railqtoken;
2000-03-28 wenzelm 2000-03-28 -I option;