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