src/HOL/Fun.ML
changeset 1776 d7e77cb8ce5c
parent 1754 852093aeb0ab
child 1822 c192d7dc22e7
     1.1 --- a/src/HOL/Fun.ML	Thu May 30 13:31:29 1996 +0200
     1.2 +++ b/src/HOL/Fun.ML	Fri May 31 19:12:00 1996 +0200
     1.3 @@ -190,20 +190,3 @@
     1.4              subsetD, subsetCE];
     1.5  
     1.6  fun cfast_tac prems = cut_facts_tac prems THEN' fast_tac set_cs;
     1.7 -
     1.8 -
     1.9 -fun prover s = prove_goal Fun.thy s (fn _=>[fast_tac set_cs 1]);
    1.10 -
    1.11 -val mem_simps = map prover
    1.12 - [ "(a : A Un B)   =  (a:A | a:B)",	(* Un_iff *)
    1.13 -   "(a : A Int B)  =  (a:A & a:B)",	(* Int_iff *)
    1.14 -   "(a : Compl(B)) =  (~a:B)",		(* Compl_iff *)
    1.15 -   "(a : A-B)      =  (a:A & ~a:B)",	(* Diff_iff *)
    1.16 -   "(a : {b})      =  (a=b)",
    1.17 -   "(a : {x.P(x)}) =  P(a)" ];
    1.18 -
    1.19 -val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs;
    1.20 -
    1.21 -simpset := !simpset addsimps mem_simps
    1.22 -                    addcongs [ball_cong,bex_cong]
    1.23 -                    setmksimps (mksimps mksimps_pairs);