src/CCL/Wfd.thy

               ALL x:A. ALL y:{y: B. <<x,y>,<p,q>>:wf(R)}. g(x,y) : D(x,y) |] ==> 
                 h(p,q,g) : D(p,q)"
   shows "letrec g x y be h(x,y,g) in g(a,b) : D(a,b)"
   apply (unfold letrec2_def)
   apply (rule SPLITB [THEN subst])
-  apply (assumption | rule letrecT pairT splitT prems)+
+  apply (assumption | rule letrecT pairT splitT assms)+
   apply (subst SPLITB)
-  apply (assumption | rule ballI SubtypeI prems)+
+  apply (assumption | rule ballI SubtypeI assms)+
   apply (rule SPLITB [THEN subst])
-  apply (assumption | rule letrecT SubtypeI pairT splitT prems |
+  apply (assumption | rule letrecT SubtypeI pairT splitT assms |
     erule bspec SubtypeE sym [THEN subst])+
   done
 
 lemma lem: "SPLIT(<a,<b,c>>,%x xs. SPLIT(xs,%y z. B(x,y,z))) = B(a,b,c)"
   by (simp add: SPLITB)

                                                         g(x,y,z) : D(x,y,z) |] ==> 
                 h(p,q,r,g) : D(p,q,r)"
   shows "letrec g x y z be h(x,y,z,g) in g(a,b,c) : D(a,b,c)"
   apply (unfold letrec3_def)
   apply (rule lem [THEN subst])
-  apply (assumption | rule letrecT pairT splitT prems)+
+  apply (assumption | rule letrecT pairT splitT assms)+
   apply (simp add: SPLITB)
-  apply (assumption | rule ballI SubtypeI prems)+
+  apply (assumption | rule ballI SubtypeI assms)+
   apply (rule lem [THEN subst])
-  apply (assumption | rule letrecT SubtypeI pairT splitT prems |
+  apply (assumption | rule letrecT SubtypeI pairT splitT assms |
     erule bspec SubtypeE sym [THEN subst])+
   done
 
 lemmas letrecTs = letrecT letrec2T letrec3T
 

 
 lemma applyV [eval]:
   assumes "f ---> lam x. b(x)"
     and "b(a) ---> c"
   shows "f ` a ---> c"
-  unfolding apply_def by (eval prems)
+  unfolding apply_def by (eval assms)
 
 lemma letV:
   assumes 1: "t ---> a"
     and 2: "f(a) ---> c"
   shows "let x be t in f(x) ---> c"