2000-11-10 wenzelm 2000-11-10 simplified atomize; added inductive_rulify2 (to accomodate malformed induction rules);
2000-11-10 wenzelm 2000-11-10 axclass power moved to Nat.thy;
2000-11-10 wenzelm 2000-11-10 added axclass inverse and consts inverse, divide (infix "/"); moved axclass power to Nat.thy;
2000-11-10 wenzelm 2000-11-10 FOL_basic_ss: simprocs moved to FOL_ss;
2000-11-10 wenzelm 2000-11-10 added atomize_eq;
2000-11-10 wenzelm 2000-11-10 val atomize = thms "atomize'";
2000-11-10 nipkow 2000-11-10 > etc
2000-11-10 nipkow 2000-11-10 new: > and >=
2000-11-10 nipkow 2000-11-10 rule inversion
2000-11-10 nipkow 2000-11-10 JMB -> JMPB. Email von Johannes Pfeifroth.
2000-11-09 wenzelm 2000-11-09 updated;
2000-11-09 wenzelm 2000-11-09 fixed \title: convert "_" to "-";
2000-11-08 wenzelm 2000-11-08 tuned isabelle environment;
2000-11-08 nipkow 2000-11-08 subgoals
2000-11-08 nipkow 2000-11-08 *** empty log message ***
2000-11-07 paulson 2000-11-07 better discussion of rule induction
2000-11-07 berghofe 2000-11-07 Thm.dest_abs now takes an additional argument.
2000-11-07 berghofe 2000-11-07 Moved rewriting functions from Thm to MetaSimplifier.
2000-11-07 berghofe 2000-11-07 - Moved rewriting functions to meta_simplifier.ML - dest_abs now also takes an optional variable name as an argument - beta_conversion takes additional flag as an argument. Fully reduces the term if set to true Some tuning: - tuned fix_shyps in instantiate, implies_intr, implies_elim, reflexive, transitive, beta_conversion, abstract_rule - combination: chktypes derives types of f and t from type of == instead of using fastype_of New primitives: - eta_conversion - incr_indexes: increment indexes in theorems - cterm_incr_indexes: increment indexes in cterms - cterm_match, cterm_first_order_match - rename_boundvars
2000-11-07 berghofe 2000-11-07 moved rewriting functions from Drule to MetaSimplifier
2000-11-07 berghofe 2000-11-07 - new theorems imp_cong and swap_prems_eq - new function dest_equals - exported strip_imp_concl - removed incr_indexes (now in Thm)
2000-11-07 berghofe 2000-11-07 Added new file meta_simplifier.ML
2000-11-07 berghofe 2000-11-07 Moved meta simplification stuff from Thm to MetaSimplifier.
2000-11-07 berghofe 2000-11-07 Added type constraint in theorem "lift".
2000-11-07 nipkow 2000-11-07 *** empty log message ***
2000-11-06 wenzelm 2000-11-06 method 'induct' now handles non-atomic goals; improved error message; option 'stripped' deprecated;
2000-11-06 wenzelm 2000-11-06 improved: 'induct' handle non-atomic goals;
2000-11-06 wenzelm 2000-11-06 make: open_parms argument;
2000-11-06 wenzelm 2000-11-06 RuleCases.make true;
2000-11-06 wenzelm 2000-11-06 added rewrite_goal_tac; resolveq_cases_tac: generalized args; tuned atomize; assm_tac: include reflexive_thm;
2000-11-06 wenzelm 2000-11-06 added typ_instance;
2000-11-06 wenzelm 2000-11-06 Sign.typ_instance;
2000-11-06 wenzelm 2000-11-06 inductive_atomize, inductive_rulify;
2000-11-06 wenzelm 2000-11-06 * Isar/HOL: method 'induct' now handles non-atomic goals; as a consequence, it is no longer monotonic wrt. the local goal context (which is now passed through the inductive cases);
2000-11-06 wenzelm 2000-11-06 tuned atomize_goal;
2000-11-06 paulson 2000-11-06 minor modifications for new Springer style
2000-11-06 paulson 2000-11-06 minor changes
2000-11-06 paulson 2000-11-06 auto update
2000-11-06 nipkow 2000-11-06 *** empty log message ***
2000-11-04 wenzelm 2000-11-04 updated;
2000-11-04 wenzelm 2000-11-04 tuned method "rule" and "default";
2000-11-04 wenzelm 2000-11-04 isamarkup: handle % in input;
2000-11-04 wenzelm 2000-11-04 tuned;
2000-11-04 wenzelm 2000-11-04 misc stuff;
2000-11-03 wenzelm 2000-11-03 tuned;
2000-11-03 wenzelm 2000-11-03 proper setup of "parallel"; removed unused rules;
2000-11-03 wenzelm 2000-11-03 tuned notation;
2000-11-03 wenzelm 2000-11-03 adapted "obtain" proofs;
2000-11-03 wenzelm 2000-11-03 provide case names for rev_induct, rev_cases;
2000-11-03 wenzelm 2000-11-03 rev_exhaust: rulify;
2000-11-03 wenzelm 2000-11-03 removed atomic_Trueprop (now in Pure/Isar/auto_bind.ML);
2000-11-03 wenzelm 2000-11-03 "atomize" for classical tactics;
2000-11-03 wenzelm 2000-11-03 atomize: all automated tactics that "solve" goals;
2000-11-03 wenzelm 2000-11-03 fixed two obscurities of "fix": predeclare_terms;
2000-11-03 wenzelm 2000-11-03 tuned names;
2000-11-03 wenzelm 2000-11-03 improved handling of "that": insert into goal, only declare as Pure "intro"; eliminated functor;
2000-11-03 wenzelm 2000-11-03 assumption / finish: handle non-atomic assumptions from context as well;
2000-11-03 wenzelm 2000-11-03 added atomic_judgment;
2000-11-03 wenzelm 2000-11-03 structure Obtain = Obtain;
2000-11-03 paulson 2000-11-03 new lemma card_Diff2_less for mulilated chess board