2001-10-13 wenzelm 2001-10-13 * Pure: added 'corollary' command;
2001-10-12 berghofe 2001-10-12 Tuned comment.
2001-10-12 berghofe 2001-10-12 - Exported goals_conv and fconv_rule - Added forall_conv
2001-10-12 wenzelm 2001-10-12 removed vars_of, concls_of; removed additional rule instantiation argument; proper enumeration of type rules; append possibilities of set and type rules (analogous to elim-intro in 'rule');
2001-10-12 wenzelm 2001-10-12 declare impE iffD1 iffD2 ad elim of Pure;
2001-10-12 wenzelm 2001-10-12 removed lookups count; always try headless rules;
2001-10-12 wenzelm 2001-10-12 added make_thm (sort-of);
2001-10-12 wenzelm 2001-10-12 added trace_rules, trace;
2001-10-12 wenzelm 2001-10-12 removed get_cases, get_induct; added find_cases[ST], finde_induct[ST]; proper indexing of types;
2001-10-12 wenzelm 2001-10-12 removed read_inst', no longer export insts';
2001-10-12 wenzelm 2001-10-12 fixed typid;
2001-10-12 wenzelm 2001-10-12 test: use SkipProof.make_thm instead of Thm.assume;
2001-10-12 wenzelm 2001-10-12 tuned;
2001-10-12 wenzelm 2001-10-12 HOLogic.dest_concls, InductAttrib.vars_of;
2001-10-12 wenzelm 2001-10-12 declare impE iffD1 iffD2 as elim of Pure;
2001-10-12 wenzelm 2001-10-12 moved trace_rules to Pure/Isar/method.ML; some_rule_tac: prefer Method.some_rule_tac of Pure, no special handling of imp_elim;
2001-10-11 wenzelm 2001-10-11 * Isar/Pure: fixed 'token_translation' command;
2001-10-11 wenzelm 2001-10-11 added try;
2001-10-11 wenzelm 2001-10-11 added certify_tyname;
2001-10-10 berghofe 2001-10-10 Exported output_symbols.
2001-10-10 berghofe 2001-10-10 Removed unnecessary application of Drule.standard.
2001-10-10 berghofe 2001-10-10 Fixed erroneous type constraint in token_translation function.
2001-10-10 berghofe 2001-10-10 Exported output_with.
2001-10-10 berghofe 2001-10-10 Tuned several functions to improve sharing of unchanged subproofs.
2001-10-09 wenzelm 2001-10-09 added global modes ref;
2001-10-08 wenzelm 2001-10-08 sane numerals (stage 3): provide generic "1" on all number types;
2001-10-08 wenzelm 2001-10-08 * added default LaTeX bindings for \<tturnstile> and \<TTurnstile>; note that these symbols are unavailable in Proof General / X-Symbol;
2001-10-08 wenzelm 2001-10-08 fixed numerals;
2001-10-08 wenzelm 2001-10-08 added tturnstile, TTurnstile;
2001-10-08 wenzelm 2001-10-08 *** empty log message ***
2001-10-08 wenzelm 2001-10-08 *** empty log message ***
2001-10-08 wenzelm 2001-10-08 replace 0r/1r by 0/1;
2001-10-08 wenzelm 2001-10-08 *** empty log message ***
2001-10-08 wenzelm 2001-10-08 fixed numerals;
2001-10-06 wenzelm 2001-10-06 * sane numerals (stage 2): plain "num" syntax (removed "#");
2001-10-05 wenzelm 2001-10-05 tuned;
2001-10-05 wenzelm 2001-10-05 *** empty log message ***
2001-10-05 wenzelm 2001-10-05 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;
2001-10-05 wenzelm 2001-10-05 *** empty log message ***
2001-10-05 wenzelm 2001-10-05 "num" syntax;
2001-10-05 wenzelm 2001-10-05 added axclass "one" and polymorphic const "1"; print consts "0" and "1" with type constraints;
2001-10-05 wenzelm 2001-10-05 added "num" token;
2001-10-05 wenzelm 2001-10-05 induct: case names;
2001-10-05 wenzelm 2001-10-05 sane spacing of "-";
2001-10-05 wenzelm 2001-10-05 tuned;
2001-10-04 wenzelm 2001-10-04 Thm.major_prem_of part of Logic.strip_assums_concl;
2001-10-04 wenzelm 2001-10-04 major_prem_of: Logic.strip_assums_concl;
2001-10-04 wenzelm 2001-10-04 induct/cases made generic, removed simplified/stripped options;
2001-10-04 wenzelm 2001-10-04 improved proof by cases and induction;
2001-10-04 wenzelm 2001-10-04 removed obsolete comment;
2001-10-04 wenzelm 2001-10-04 generic induct_method.ML; tuned;
2001-10-04 wenzelm 2001-10-04 non-oriented infix = and ~= (output only); added case_split (with case names);
2001-10-04 wenzelm 2001-10-04 $(SRC)/Provers/induct_method.ML replaces Tools/induct_method.ML;
2001-10-04 wenzelm 2001-10-04 use "~~/src/Provers/induct_method.ML";
2001-10-04 wenzelm 2001-10-04 removed hol_rewrite_cterm (use full_rewrite_cterm from Pure);
2001-10-04 wenzelm 2001-10-04 added dest_concls;
2001-10-04 wenzelm 2001-10-04 simp_case_tac is back again from induct_method.ML; tuned;
2001-10-04 wenzelm 2001-10-04 made generic (see Provers/induct_method.ML);
2001-10-04 wenzelm 2001-10-04 qualify MetaSimplifier;
2001-10-04 wenzelm 2001-10-04 unsymbolized;