2001-10-31 ago berghofe Additional rules for simplifying inside "Goal"
2001-10-31 ago berghofe - Tuned add_cnstrt
2001-10-31 ago berghofe Removed name_thm from finish_global.
2001-10-31 ago berghofe Tuned function thm_proof.
2001-10-31 ago berghofe - enter_thmx -> enter_thms
2001-10-31 ago berghofe norm_hhf_eq is now stored using open_store_standard_thm.
2001-10-31 ago wenzelm induct: internalize ``missing'' consumes-facts from goal state
2001-10-31 ago wenzelm - 'induct' may now use elim-style induction rules without chaining
2001-10-31 ago wenzelm (induct set: ...);
2001-10-31 ago wenzelm put_consumes: really overwrite existing tag;
2001-10-31 ago wenzelm finish_global: Tactic.norm_hhf;
2001-10-31 ago wenzelm use HOL.induct_XXX;
2001-10-31 ago wenzelm use induct_rulify2;
2001-10-31 ago wenzelm renamed inductive_XXX to induct_XXX;
2001-10-31 ago wenzelm induct_impliesI;
2001-10-30 ago wenzelm tuned induct proofs;
2001-10-30 ago wenzelm - 'induct' method now derives symbolic cases from the *rulified* rule
2001-10-30 ago wenzelm tuned;
2001-10-30 ago wenzelm induct: cases are extracted from rulified rule;
2001-10-30 ago wenzelm removed obsolete make_raw;
2001-10-30 ago wenzelm lemma Least_mono moved from Typedef.thy to Set.thy;
2001-10-29 ago wenzelm tuned;
2001-10-29 ago wenzelm removed option -depend (not available everywhere?);
2001-10-28 ago wenzelm converted theory "Set";
2001-10-28 ago wenzelm fixed string_of_mixfix;
2001-10-28 ago wenzelm tuned declaration of rules;
2001-10-28 ago wenzelm equal_intr_rule already declared in Pure;
2001-10-28 ago wenzelm rules for meta-level conjunction;
2001-10-28 ago wenzelm tuned prove;
2001-10-27 ago wenzelm tuned;
2001-10-27 ago wenzelm added prove;
2001-10-27 ago wenzelm declare equal_intr_rule as intro;
2001-10-27 ago wenzelm tuned prove;
2001-10-27 ago wenzelm removed obsolete goal_subclass, goal_arity;
2001-10-27 ago wenzelm use Tactic.prove;
2001-10-27 ago wenzelm use Tactic.prove;
2001-10-27 ago wenzelm tuned;
2001-10-27 ago wenzelm * Pure/axclass: removed obsolete ML interface goal_subclass/goal_arity;
2001-10-27 ago wenzelm updated;
2001-10-27 ago wenzelm impose hyps on initial goal configuration (prevents res_inst_tac problems);
2001-10-27 ago wenzelm added "atomize" method;
2001-10-27 ago wenzelm prove: primitive goal interface for internal use;
2001-10-27 ago wenzelm added impose_hyps;
2001-10-27 ago wenzelm exclude field_simps from user-level "simps";
2001-10-27 ago wenzelm Isar: fixed rep_datatype args;
2001-10-27 ago wenzelm hardwire qualified const names;
2001-10-27 ago wenzelm removed "more" class;
2001-10-27 ago wenzelm moved product cases/induct to theory Datatype;
2001-10-27 ago wenzelm made new-style theory;
2001-10-26 ago wenzelm atomize_conj;
2001-10-26 ago wenzelm * Pure: method 'atomize' presents local goal premises as object-level
2001-10-26 ago berghofe Fixed several bugs concerning arbitrarily branching datatypes.
2001-10-26 ago berghofe Eliminated occurrence of rule_format.
2001-10-26 ago wenzelm tuned;
2001-10-26 ago wenzelm need at least 3 latex runs to get toc right!
2001-10-26 ago wenzelm tuned;
2001-10-26 ago wenzelm tuned;
2001-10-26 ago wenzelm Rrightarrow;
2001-10-26 ago wenzelm tuned notation;
2001-10-26 ago wenzelm tuned notation;