1997-03-05 wenzelm 1997-03-05 *** empty log message ***
1997-03-05 paulson 1997-03-05 Added comment
1997-03-05 paulson 1997-03-05 Now uses eta_contract_atom for greater speed
1997-03-05 paulson 1997-03-05 Eta-expanded declarations of addSIs2, etc., to avoid polymorphism errors
1997-03-05 paulson 1997-03-05 HOL: renaming of "not"
1997-03-05 paulson 1997-03-05 Declares eta_contract_atom; fixed comment; some tidying
1997-03-05 paulson 1997-03-05 Added comment
1997-03-05 paulson 1997-03-05 Now declares needs_filtered_use, but still unusable with current MLWorks
1997-03-05 paulson 1997-03-05 Now uses rotate_tac and eta_contract_atom for greater speed
1997-03-05 paulson 1997-03-05 New version of InterE, like its ZF counterpart
1997-03-05 paulson 1997-03-05 Renamed constant "not" to "Not"
1997-03-04 paulson 1997-03-04 Renamed constant "not" to "Not"
1997-03-04 paulson 1997-03-04 Renamed constant "not" to "Not"
1997-03-04 paulson 1997-03-04 best_tac avoids looping with change to RepFun_eqI in claset
1997-03-04 paulson 1997-03-04 Now uses RepFun_eqI instead of RepFunI; improved version of InterE to replace "make_elim InterD" in claset
1997-03-04 paulson 1997-03-04 Updated reference to Pelletier erratum
1997-03-04 paulson 1997-03-04 Removed needless quotes
1997-03-03 wenzelm 1997-03-03 removed bash debug;
1997-03-03 wenzelm 1997-03-03 removed -r option; added -p option;
1997-03-03 wenzelm 1997-03-03 fixed -m order;
1997-03-03 wenzelm 1997-03-03 improved xterm, xterm_color;
1997-03-03 wenzelm 1997-03-03 added comment;
1997-03-03 wenzelm 1997-03-03 added comment: print translations do not mark tokens;
1997-03-01 wenzelm 1997-03-01 added color styles; refs for test;
1997-02-28 wenzelm 1997-02-28 improved err msg;
1997-02-28 wenzelm 1997-02-28 *** empty log message ***
1997-02-28 wenzelm 1997-02-28 more robust handling of invocation errors; added -m MODE option;
1997-02-28 wenzelm 1997-02-28 more robust handling of invocation errors;
1997-02-28 wenzelm 1997-02-28 now uses -m symbols;
1997-02-28 wenzelm 1997-02-28 split ast_of_term(T); ast_of_term now marks frees; added token translation support;
1997-02-28 wenzelm 1997-02-28 added token translation support;
1997-02-28 wenzelm 1997-02-28 term_of_... now mark class, tfree, tvar;
1997-02-28 wenzelm 1997-02-28 added mark_bound(T), variant_abs'; trfuns now mark bounds they introduce!! added pure_trfunsT;
1997-02-28 wenzelm 1997-02-28 Token translations for xterm and LaTeX output.
1997-02-28 wenzelm 1997-02-28 added _mk_ofclass(S);
1997-02-28 wenzelm 1997-02-28 added strlen (includes metric information); removed map_strs;
1997-02-28 wenzelm 1997-02-28 added token_translation interface;
1997-02-28 wenzelm 1997-02-28 added add_tokentrfuns;
1997-02-28 wenzelm 1997-02-28 added Syntax/token_trans.ML;
1997-02-28 wenzelm 1997-02-28 added token_trans.ML;
1997-02-28 paulson 1997-02-28 Slightly more robust proof
1997-02-28 paulson 1997-02-28 dup_intr & dup_elim no longer call standard -- this lets them be used on meta-hyps
1997-02-28 paulson 1997-02-28 rule_by_tactic no longer standardizes its result
1997-02-28 paulson 1997-02-28 Addition of de Bruijn formulae
1997-02-27 wenzelm 1997-02-27 tuned comment;
1997-02-27 wenzelm 1997-02-27 tuned comments;
1997-02-25 wenzelm 1997-02-25 added proper subset symbols syntax;
1997-02-25 pusch 1997-02-25 minor changes due to primrec defintions for +,-,*
1997-02-25 pusch 1997-02-25 minor changes due to new primrec definitions for +,-,*
1997-02-25 pusch 1997-02-25 definitions of +,-,* replaced by primrec definitions
1997-02-25 pusch 1997-02-25 function nat_add_primrec added to allow primrec definitions over nat
1997-02-24 oheimb 1997-02-24 removed explicit_domains/, which is now covered by ex/
1997-02-24 wenzelm 1997-02-24 added "_" syntax for dummyT;
1997-02-21 wenzelm 1997-02-21 declared the dummy type;
1997-02-21 wenzelm 1997-02-21 replaced natural by subset;
1997-02-21 wenzelm 1997-02-21 tuned symbolic [|_|] syntax;
1997-02-21 wenzelm 1997-02-21 tuned some chars;
1997-02-21 paulson 1997-02-21 More robust proof (?)
1997-02-21 paulson 1997-02-21 Replaced "flat" by the Basis Library function List.concat
1997-02-21 paulson 1997-02-21 Introduction of rotate_rule