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;
2001-10-04 wenzelm 2001-10-04 moved atomize stuff to theory IFOL; added induct/cases setup;
2001-10-04 wenzelm 2001-10-04 atomize stuff from theory FOL; tuned;
2001-10-04 wenzelm 2001-10-04 added Provers/induct_method.ML, document/root.tex, ex/Natural_Numbers.thy;
2001-10-04 wenzelm 2001-10-04 theory Natural_Numbers;
2001-10-04 wenzelm 2001-10-04 use "~~/src/Provers/induct_method.ML";
2001-10-04 wenzelm 2001-10-04 Theory of the natural numbers: Peano's axioms, primitive recursion. (Modernized version of Larry Paulson's theory "Nat".)
2001-10-04 wenzelm 2001-10-04 full_rewrite_cterm_aux (see also tactic.ML); no longer open MetaSimplifier;
2001-10-04 wenzelm 2001-10-04 added full_rewrite_cterm;
2001-10-04 wenzelm 2001-10-04 proof by cases and induction on types and sets (used to be specific for HOL);
2001-10-04 wenzelm 2001-10-04 qualify MetaSimplifier;
2001-10-04 wenzelm 2001-10-04 added dest_conj, dest_concls;
2001-10-04 wenzelm 2001-10-04 document setup;
2001-10-04 wenzelm 2001-10-04 added print_induct_rules;
2001-10-04 wenzelm 2001-10-04 tuned print operation;
2001-10-04 wenzelm 2001-10-04 tuned;
2001-10-04 wenzelm 2001-10-04 * moved induct/cases attributes to Pure, added 'print_induct_rules' command;
2001-10-04 wenzelm 2001-10-04 print_induct_rules;
2001-10-04 wenzelm 2001-10-04 updated;
2001-10-04 berghofe 2001-10-04 Fixed bug in decompose.
2001-10-03 wenzelm 2001-10-03 Tools/induct_attrib.ML now part of Pure;
2001-10-03 wenzelm 2001-10-03 Isar/induct_attrib.ML;
2001-10-03 wenzelm 2001-10-03 *** empty log message ***
2001-10-03 wenzelm 2001-10-03 moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
2001-10-03 wenzelm 2001-10-03 tuned parentheses in relational expressions;
2001-10-03 wenzelm 2001-10-03 moved linorder_cases to theory Ord;
2001-10-03 wenzelm 2001-10-03 linorder_cases supersedes linorder_less_split; tuned parentheses in relational expressions;
2001-10-03 paulson 2001-10-03 eta-expansion required for SML/NJ
2001-10-02 wenzelm 2001-10-02 support non-oriented infix;
2001-10-01 wenzelm 2001-10-01 tuned;
2001-10-01 wenzelm 2001-10-01 tuned;
2001-10-01 wenzelm 2001-10-01 *** empty log message ***
2001-10-01 wenzelm 2001-10-01 initial setup for chapter on document preparation;
2001-10-01 wenzelm 2001-10-01 updated output;
2001-10-01 streckem 2001-10-01 - declared wf_java_prog as syntax (previously: definition) - in wf_java_mdecl: added preconditions for 'This' - rule LAss: precondition v ~=This
2001-10-01 streckem 2001-10-01 Removed some unfoldings of defs after declaring wf_java_prog as syntax
2001-10-01 streckem 2001-10-01 Added axiom e~=This to reflect strengthened precond. in rule LAss
2001-10-01 streckem 2001-10-01 Minor modifications
2001-10-01 wenzelm 2001-10-01 added Ordinals example;
2001-09-30 berghofe 2001-09-30 Tuned indentation of abstractions.
2001-09-28 wenzelm 2001-09-28 tuned;
2001-09-28 wenzelm 2001-09-28 inductive: no collective atts;
2001-09-28 wenzelm 2001-09-28 inductive: no collective atts;
2001-09-28 wenzelm 2001-09-28 oops;
2001-09-28 wenzelm 2001-09-28 tuned;
2001-09-28 wenzelm 2001-09-28 recdef (permissive); inductive: no collective atts;
2001-09-28 wenzelm 2001-09-28 *** empty log message ***
2001-09-28 wenzelm 2001-09-28 prove: ``strict'' argument;
2001-09-28 wenzelm 2001-09-28 internal thm numbering with ":" instead of "_";
2001-09-28 wenzelm 2001-09-28 avoid handle _;