src/HOL/simpdata.ML
changeset 9894 c8ff37b637a7
parent 9876 a069795f1060
child 9969 4753185f1dd2
     1.1 --- a/src/HOL/simpdata.ML	Thu Sep 07 20:51:07 2000 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Thu Sep 07 20:51:31 2000 +0200
     1.3 @@ -432,37 +432,6 @@
     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 rulify_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