# HG changeset patch # User Cezary Kaliszyk # Date 1273148025 -7200 # Node ID c1edd05f207fd467460d734e3104b2539587bc4e # Parent 1c866b53eb3c4167d6ebb25c2b9b46bb1d049d72# Parent db218886e67455ba5519c62ad1726410d8b7e38d merge diff -r 1c866b53eb3c -r c1edd05f207f Nominal-General/nominal_eqvt.ML --- a/Nominal-General/nominal_eqvt.ML Thu May 06 14:13:35 2010 +0200 +++ b/Nominal-General/nominal_eqvt.ML Thu May 06 14:13:45 2010 +0200 @@ -77,7 +77,7 @@ let fun split_conj names (Const ("op &", _) $ f1 $ f2) = (case head_of f1 of - Const (name, _) => if name mem names then SOME f2 else NONE + Const (name, _) => if member (op =) names name then SOME f2 else NONE | _ => NONE) | split_conj _ _ = NONE; in @@ -178,4 +178,4 @@ K.thy_decl (P.xname >> equivariance); end; -end (* structure *) \ No newline at end of file +end (* structure *) diff -r 1c866b53eb3c -r c1edd05f207f Nominal-General/nominal_permeq.ML --- a/Nominal-General/nominal_permeq.ML Thu May 06 14:13:35 2010 +0200 +++ b/Nominal-General/nominal_permeq.ML Thu May 06 14:13:45 2010 +0200 @@ -117,7 +117,7 @@ let val hd = head_of trm in - if is_Const hd andalso (fst (dest_Const hd)) mem bad_hds then () + if is_Const hd andalso member (op =) bad_hds (fst (dest_Const hd)) then () else (if strict_flag then error else warning) ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm)) end @@ -183,4 +183,4 @@ fun perm_strict_simp_meth (thms, consts) ctxt = SIMPLE_METHOD (HEADGOAL (eqvt_strict_tac ctxt thms consts)) -end; (* structure *) \ No newline at end of file +end; (* structure *) diff -r 1c866b53eb3c -r c1edd05f207f Nominal/Equivp.thy --- a/Nominal/Equivp.thy Thu May 06 14:13:35 2010 +0200 +++ b/Nominal/Equivp.thy Thu May 06 14:13:45 2010 +0200 @@ -56,7 +56,7 @@ split_conj_tac THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW split_conj_tac THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps @{thms alphas fresh_star_def fresh_zero_perm permute_zero ball_triv - add_0_left supp_zero_perm Int_empty_left split_conv}) + add_0_left supp_zero_perm Int_empty_left split_conv prod_rel.simps}) *} ML {* @@ -291,7 +291,7 @@ ML {* fun choose_alpha_abs eqiff = let - fun exists_subterms f ts = true mem (map (exists_subterm f) ts); + fun exists_subterms f ts = member (op =) (map (exists_subterm f) ts) true; val terms = map prop_of eqiff; fun check cname = exists_subterms (fn x => fst(dest_Const x) = cname handle _ => false) terms val no = diff -r 1c866b53eb3c -r c1edd05f207f Nominal/NewFv.thy --- a/Nominal/NewFv.thy Thu May 06 14:13:35 2010 +0200 +++ b/Nominal/NewFv.thy Thu May 06 14:13:45 2010 +0200 @@ -140,7 +140,7 @@ val non_rec_vars = case binds of [(SOME bn, i)] => - if i mem bodys + if member (op =) bodys i then noatoms else ((the (AList.lookup (op=) bn_fvbn bn)) $ nth args i) | _ => noatoms diff -r 1c866b53eb3c -r c1edd05f207f Nominal/Rsp.thy --- a/Nominal/Rsp.thy Thu May 06 14:13:35 2010 +0200 +++ b/Nominal/Rsp.thy Thu May 06 14:13:45 2010 +0200 @@ -63,7 +63,7 @@ rel_indtac induct THEN_ALL_NEW (TRY o rtac @{thm TrueI}) THEN_ALL_NEW asm_full_simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW - asm_full_simp_tac (HOL_ss addsimps (@{thms alphas} @ fvbv_simps)) THEN_ALL_NEW + asm_full_simp_tac (HOL_ss addsimps (@{thms alphas prod_rel.simps prod_fv.simps} @ fvbv_simps)) THEN_ALL_NEW REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps fvbv_simps) THEN_ALL_NEW TRY o blast_tac (claset_of ctxt) @@ -83,7 +83,7 @@ REPEAT o rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps (rsp @ - @{thms split_conv alphas fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left})) + @{thms split_conv alphas fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left prod_rel.simps prod_fv.simps})) )) *}