2001-10-12 ago wenzelm moved trace_rules to Pure/Isar/method.ML;
2001-10-11 ago wenzelm * Isar/Pure: fixed 'token_translation' command;
2001-10-11 ago wenzelm added try;
2001-10-11 ago wenzelm added certify_tyname;
2001-10-10 ago berghofe Exported output_symbols.
2001-10-10 ago berghofe Removed unnecessary application of Drule.standard.
2001-10-10 ago berghofe Fixed erroneous type constraint in token_translation function.
2001-10-10 ago berghofe Exported output_with.
2001-10-10 ago berghofe Tuned several functions to improve sharing of unchanged subproofs.
2001-10-09 ago wenzelm added global modes ref;
2001-10-08 ago wenzelm sane numerals (stage 3): provide generic "1" on all number types;
2001-10-08 ago wenzelm * added default LaTeX bindings for \<tturnstile> and \<TTurnstile>;
2001-10-08 ago wenzelm fixed numerals;
2001-10-08 ago wenzelm added tturnstile, TTurnstile;
2001-10-08 ago wenzelm *** empty log message ***
2001-10-08 ago wenzelm *** empty log message ***
2001-10-08 ago wenzelm replace 0r/1r by 0/1;
2001-10-08 ago wenzelm *** empty log message ***
2001-10-08 ago wenzelm fixed numerals;
2001-10-06 ago wenzelm * sane numerals (stage 2): plain "num" syntax (removed "#");
2001-10-05 ago wenzelm tuned;
2001-10-05 ago wenzelm *** empty log message ***
2001-10-05 ago wenzelm sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
2001-10-05 ago wenzelm *** empty log message ***
2001-10-05 ago wenzelm "num" syntax;
2001-10-05 ago wenzelm added axclass "one" and polymorphic const "1";
2001-10-05 ago wenzelm added "num" token;
2001-10-05 ago wenzelm induct: case names;
2001-10-05 ago wenzelm sane spacing of "-";
2001-10-05 ago wenzelm tuned;
2001-10-04 ago wenzelm Thm.major_prem_of part of Logic.strip_assums_concl;
2001-10-04 ago wenzelm major_prem_of: Logic.strip_assums_concl;
2001-10-04 ago wenzelm induct/cases made generic, removed simplified/stripped options;
2001-10-04 ago wenzelm improved proof by cases and induction;
2001-10-04 ago wenzelm removed obsolete comment;
2001-10-04 ago wenzelm generic induct_method.ML;
2001-10-04 ago wenzelm non-oriented infix = and ~= (output only);
2001-10-04 ago wenzelm $(SRC)/Provers/induct_method.ML replaces Tools/induct_method.ML;
2001-10-04 ago wenzelm use "~~/src/Provers/induct_method.ML";
2001-10-04 ago wenzelm removed hol_rewrite_cterm (use full_rewrite_cterm from Pure);
2001-10-04 ago wenzelm added dest_concls;
2001-10-04 ago wenzelm simp_case_tac is back again from induct_method.ML;
2001-10-04 ago wenzelm made generic (see Provers/induct_method.ML);
2001-10-04 ago wenzelm qualify MetaSimplifier;
2001-10-04 ago wenzelm unsymbolized;
2001-10-04 ago wenzelm moved atomize stuff to theory IFOL;
2001-10-04 ago wenzelm atomize stuff from theory FOL;
2001-10-04 ago wenzelm added Provers/induct_method.ML, document/root.tex, ex/Natural_Numbers.thy;
2001-10-04 ago wenzelm theory Natural_Numbers;
2001-10-04 ago wenzelm use "~~/src/Provers/induct_method.ML";
2001-10-04 ago wenzelm Theory of the natural numbers: Peano's axioms, primitive recursion.
2001-10-04 ago wenzelm full_rewrite_cterm_aux (see also tactic.ML);
2001-10-04 ago wenzelm added full_rewrite_cterm;
2001-10-04 ago wenzelm proof by cases and induction on types and sets (used to be specific for HOL);
2001-10-04 ago wenzelm qualify MetaSimplifier;
2001-10-04 ago wenzelm added dest_conj, dest_concls;
2001-10-04 ago wenzelm document setup;
2001-10-04 ago wenzelm added print_induct_rules;
2001-10-04 ago wenzelm tuned print operation;
2001-10-04 ago wenzelm tuned;