src/CCL/CCL.thy
changeset 39159 0dec18004e75
parent 36452 d37c6eed8117
child 40844 5895c525739d
     1.1 --- a/src/CCL/CCL.thy	Mon Sep 06 19:11:01 2010 +0200
     1.2 +++ b/src/CCL/CCL.thy	Mon Sep 06 19:13:10 2010 +0200
     1.3 @@ -238,9 +238,9 @@
     1.4  
     1.5    fun mk_thm_str thy a b = "~ " ^ (saturate thy a "a") ^ " = " ^ (saturate thy b "b")
     1.6  
     1.7 -  val lemma = thm "lem";
     1.8 -  val eq_lemma = thm "eq_lemma";
     1.9 -  val distinctness = thm "distinctness";
    1.10 +  val lemma = @{thm lem};
    1.11 +  val eq_lemma = @{thm eq_lemma};
    1.12 +  val distinctness = @{thm distinctness};
    1.13    fun mk_lemma (ra,rb) = [lemma] RL [ra RS (rb RS eq_lemma)] RL
    1.14                             [distinctness RS notE, @{thm sym} RS (distinctness RS notE)]
    1.15  in