src/HOL/simpdata.ML
changeset 9736 332fab43628f
parent 9713 2c5b42311eb0
child 9801 5e7c4a45d8bb
     1.1 --- a/src/HOL/simpdata.ML	Tue Aug 29 22:31:36 2000 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Wed Aug 30 10:21:19 2000 +0200
     1.3 @@ -480,6 +480,37 @@
     1.4  val simpsetup =
     1.5    [fn thy => (simpset_ref_of thy := HOL_ss addcongs [if_weak_cong]; thy)];
     1.6  
     1.7 +(*** conversion of -->/! into ==>/!! ***)
     1.8 +
     1.9 +local
    1.10 +  val rules = [symmetric(thm"all_eq"),symmetric(thm"imp_eq"),Drule.norm_hhf_eq]
    1.11 +  val ss = HOL_basic_ss addsimps rules
    1.12 +in
    1.13 +
    1.14 +val rulify = zero_var_indexes o strip_shyps_warning o forall_elim_vars_safe o simplify ss;
    1.15 +
    1.16 +fun qed_spec_mp name = ThmDatabase.ml_store_thm(name, rulify(result()));
    1.17 +
    1.18 +fun qed_goal_spec_mp name thy s p = 
    1.19 +	bind_thm (name, rulify (prove_goal thy s p));
    1.20 +
    1.21 +fun qed_goalw_spec_mp name thy defs s p = 
    1.22 +	bind_thm (name, rulify (prove_goalw thy defs s p));
    1.23 +
    1.24 +end;
    1.25 +
    1.26 +local
    1.27 +
    1.28 +fun gen_rulify x =
    1.29 +  Attrib.no_args (Drule.rule_attribute (fn _ => rulify)) x;
    1.30 +
    1.31 +in
    1.32 +
    1.33 +val attrib_setup =
    1.34 + [Attrib.add_attributes
    1.35 +  [("rulify", (gen_rulify, gen_rulify), "put theorem into standard rule form")]];
    1.36 +
    1.37 +end;
    1.38  
    1.39  (*** integration of simplifier with classical reasoner ***)
    1.40