Enforced partial evaluation of mk_case_split_tac
authornipkow
Wed Mar 08 12:56:45 1995 +0100 (1995-03-08)
changeset 941f8a202891ac9
parent 940 bd9ab32bfa30
child 942 d9edeb96b51c
Enforced partial evaluation of mk_case_split_tac
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/simpdata.ML	Wed Mar 08 12:37:59 1995 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Wed Mar 08 12:56:45 1995 +0100
     1.3 @@ -111,8 +111,11 @@
     1.4        addsimps ([if_True, if_False, o_apply, conj_assoc] @ simp_thms)
     1.5        addcongs [imp_cong];
     1.6  
     1.7 -fun split_tac splits =
     1.8 -  mk_case_split_tac (meta_eq_to_obj_eq RS iffD2) (map mk_meta_eq splits);
     1.9 +local val mktac = mk_case_split_tac (meta_eq_to_obj_eq RS iffD2)
    1.10 +in
    1.11 +fun split_tac splits = mktac (map mk_meta_eq splits)
    1.12 +end;
    1.13 +
    1.14  
    1.15  (* eliminiation of existential quantifiers in assumptions *)
    1.16