2001-11-03 wenzelm 2001-11-03 updated;
2001-11-03 wenzelm 2001-11-03 tuned;
2001-11-03 wenzelm 2001-11-03 proper use of bind_thm(s);
2001-11-03 wenzelm 2001-11-03 adapted to new-style theories;
2001-11-03 wenzelm 2001-11-03 GPLed;
2001-11-03 wenzelm 2001-11-03 converted theory Dnat;
2001-11-03 wenzelm 2001-11-03 * 'domain' package adapted to new-style theories, e.g. see HOLCF/ex/Dnat.thy;
2001-11-03 wenzelm 2001-11-03 document setup;
2001-11-03 wenzelm 2001-11-03 replaced Undef by UU;
2001-11-03 wenzelm 2001-11-03 ax_flat;
2001-11-03 wenzelm 2001-11-03 GPLed;
2001-11-03 wenzelm 2001-11-03 tuned;
2001-11-03 wenzelm 2001-11-03 replaced Undef by UU;
2001-11-03 wenzelm 2001-11-03 converted theory Lift;
2001-11-03 wenzelm 2001-11-03 rep_datatype lift; converted to new-style theory;
2001-11-03 wenzelm 2001-11-03 moved into Main;
2001-11-03 wenzelm 2001-11-03 moved String into Main;
2001-11-03 wenzelm 2001-11-03 tuned;
2001-11-03 wenzelm 2001-11-03 HOLCF: proper rep_datatype lift (see theory Lift); use plain induct_tac instead of lift.induct_tac, use UU instead of Undef in cases;
2001-11-02 wenzelm 2001-11-02 declare transitive;
2001-11-02 wenzelm 2001-11-02 theory Calculation move to Set;
2001-11-02 wenzelm 2001-11-02 transitive declared in Pure;
2001-11-02 paulson 2001-11-02 Numerals and simprocs for types real and hypreal. The abstract constants 0, 1 and binary numerals work harmoniously.
2001-11-01 wenzelm 2001-11-01 Goals.add_locale;
2001-11-01 wenzelm 2001-11-01 fix_frees; improved export_def: handle args on lhs;
2001-11-01 wenzelm 2001-11-01 theorem: locale argument;
2001-11-01 wenzelm 2001-11-01 beginnings of new locales (not yet functional);
2001-11-01 wenzelm 2001-11-01 Goals.setup;
2001-11-01 wenzelm 2001-11-01 parking code for old-style locales here;
2001-10-31 wenzelm 2001-10-31 tuned notation (degree instead of dollar);
2001-10-31 wenzelm 2001-10-31 theorem(_i): locale argument; contexts 0 and 1 in state now refer to theory and locale, respectively; unified export (no longer uses global "standard");
2001-10-31 wenzelm 2001-10-31 Proof.init_state thy None;
2001-10-31 wenzelm 2001-10-31 simplified export; tuned printing of fixes;
2001-10-31 wenzelm 2001-10-31 'atomize': CHANGED_PROP;
2001-10-31 wenzelm 2001-10-31 global statements: locale argument;
2001-10-31 wenzelm 2001-10-31 added local_standard;
2001-10-31 wenzelm 2001-10-31 IsarThy.theorem_i: no locale;
2001-10-31 wenzelm 2001-10-31 removed obsolete (rule equal_intr_rule);
2001-10-31 berghofe 2001-10-31 Additional rules for simplifying inside "Goal"
2001-10-31 berghofe 2001-10-31 - Tuned add_cnstrt - Fixed bug in reconstruct_proof that caused infinite loop
2001-10-31 berghofe 2001-10-31 Removed name_thm from finish_global.
2001-10-31 berghofe 2001-10-31 Tuned function thm_proof.
2001-10-31 berghofe 2001-10-31 - enter_thmx -> enter_thms - improved naming of theorems: enter_thms now takes functions pre_name and post_name as arguments
2001-10-31 berghofe 2001-10-31 norm_hhf_eq is now stored using open_store_standard_thm.
2001-10-31 wenzelm 2001-10-31 induct: internalize ``missing'' consumes-facts from goal state (enables unstructured scripts to perform elim-style induction);
2001-10-31 wenzelm 2001-10-31 - 'induct' may now use elim-style induction rules without chaining facts, using ``missing'' premises from the goal state; this allows rules stemming from inductive sets to be applied in unstructured scripts, while still benefitting from proper handling of non-atomic statements; NB: major inductive premises need to be put first, all the rest of the goal is passed through the induction;
2001-10-31 wenzelm 2001-10-31 (induct set: ...);
2001-10-31 wenzelm 2001-10-31 put_consumes: really overwrite existing tag;
2001-10-31 wenzelm 2001-10-31 finish_global: Tactic.norm_hhf;
2001-10-31 wenzelm 2001-10-31 use HOL.induct_XXX;
2001-10-31 wenzelm 2001-10-31 use induct_rulify2;
2001-10-31 wenzelm 2001-10-31 renamed inductive_XXX to induct_XXX; added induct_impliesI;
2001-10-31 wenzelm 2001-10-31 induct_impliesI;
2001-10-30 wenzelm 2001-10-30 tuned induct proofs;
2001-10-30 wenzelm 2001-10-30 - 'induct' method now derives symbolic cases from the *rulified* rule (before it used to rulify cases stemming from the internal atomized version); this means that the context of a non-atomic statement becomes is included in the hypothesis, avoiding the slightly cumbersome show "PROP ?case" form;
2001-10-30 wenzelm 2001-10-30 tuned;
2001-10-30 wenzelm 2001-10-30 induct: cases are extracted from rulified rule;
2001-10-30 wenzelm 2001-10-30 removed obsolete make_raw;
2001-10-30 wenzelm 2001-10-30 lemma Least_mono moved from Typedef.thy to Set.thy;
2001-10-29 wenzelm 2001-10-29 tuned;