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;
2000-03-27 ago wenzelm renamed 'hoare_vcg' to 'hoare';
2000-03-27 ago wenzelm tuned;
2000-03-27 ago wenzelm fixed dddot_tr;
2000-03-27 ago wenzelm rail token vs. terminal;
2000-03-27 ago wenzelm fixed term syntax;
2000-03-27 ago wenzelm tail token vs. terminal;
2000-03-27 ago wenzelm fixed \rail@tokenfont (ever used?);
2000-03-27 ago paulson added an order-sorted version of quickSort
2000-03-27 ago paulson simplified constant "colored"
2000-03-26 ago wenzelm added 'ultimately';
2000-03-26 ago wenzelm added WhileRule';
2000-03-26 ago wenzelm made SML/NJ happy;
2000-03-26 ago wenzelm tuned presentation;
2000-03-26 ago wenzelm tuned;