proper antiquotations;
authorwenzelm
Tue Apr 26 22:18:07 2011 +0200 (2011-04-26)
changeset 42480f4f011d1bf0b
parent 42479 b7c9f09d4d88
child 42481 54450fa0d78b
proper antiquotations;
src/CCL/CCL.thy
src/CCL/Type.thy
     1.1 --- a/src/CCL/CCL.thy	Tue Apr 26 21:55:11 2011 +0200
     1.2 +++ b/src/CCL/CCL.thy	Tue Apr 26 22:18:07 2011 +0200
     1.3 @@ -245,8 +245,9 @@
     1.4    val lemma = @{thm lem};
     1.5    val eq_lemma = @{thm eq_lemma};
     1.6    val distinctness = @{thm distinctness};
     1.7 -  fun mk_lemma (ra,rb) = [lemma] RL [ra RS (rb RS eq_lemma)] RL
     1.8 -                           [distinctness RS notE, @{thm sym} RS (distinctness RS notE)]
     1.9 +  fun mk_lemma (ra,rb) =
    1.10 +    [lemma] RL [ra RS (rb RS eq_lemma)] RL
    1.11 +    [distinctness RS @{thm notE}, @{thm sym} RS (distinctness RS @{thm notE})]
    1.12  in
    1.13    fun mk_lemmas rls = maps mk_lemma (mk_combs pair rls)
    1.14    fun mk_dstnct_rls thy xs = mk_combs (mk_thm_str thy) xs
    1.15 @@ -279,15 +280,15 @@
    1.16  
    1.17  (*** Rewriting and Proving ***)
    1.18  
    1.19 -fun XH_to_I rl = rl RS iffD2
    1.20 -fun XH_to_D rl = rl RS iffD1
    1.21 +fun XH_to_I rl = rl RS @{thm iffD2}
    1.22 +fun XH_to_D rl = rl RS @{thm iffD1}
    1.23  val XH_to_E = make_elim o XH_to_D
    1.24  val XH_to_Is = map XH_to_I
    1.25  val XH_to_Ds = map XH_to_D
    1.26  val XH_to_Es = map XH_to_E;
    1.27  
    1.28  bind_thms ("ccl_rews", @{thms caseBs} @ @{thms ccl_injs} @ ccl_dstncts);
    1.29 -bind_thms ("ccl_dstnctsEs", ccl_dstncts RL [notE]);
    1.30 +bind_thms ("ccl_dstnctsEs", ccl_dstncts RL [@{thm notE}]);
    1.31  bind_thms ("ccl_injDs", XH_to_Ds @{thms ccl_injs});
    1.32  *}
    1.33  
     2.1 --- a/src/CCL/Type.thy	Tue Apr 26 21:55:11 2011 +0200
     2.2 +++ b/src/CCL/Type.thy	Tue Apr 26 22:18:07 2011 +0200
     2.3 @@ -417,10 +417,10 @@
     2.4  
     2.5  ML {*
     2.6  fun genIs_tac ctxt genXH gen_mono =
     2.7 -  rtac (genXH RS iffD2) THEN'
     2.8 +  rtac (genXH RS @{thm iffD2}) THEN'
     2.9    simp_tac (simpset_of ctxt) THEN'
    2.10    TRY o fast_tac (claset_of ctxt addIs
    2.11 -        [genXH RS iffD2, gen_mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}])
    2.12 +        [genXH RS @{thm iffD2}, gen_mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}])
    2.13  *}
    2.14  
    2.15  method_setup genIs = {*