src/CCL/Fix.thy

       apply simp_all
   done
 
 (* All fixed points are lam-expressions *)
 
-schematic_lemma idgenfp_lam: "idgen(d) = d \<Longrightarrow> d = lam x. ?f(x)"
+schematic_goal idgenfp_lam: "idgen(d) = d \<Longrightarrow> d = lam x. ?f(x)"
   apply (unfold idgen_def)
   apply (erule ssubst)
   apply (rule refl)
   done
 

   apply (erule ssubst)
   apply (rule po_lam [THEN iffD2])
   apply simp
   done
 
-schematic_lemma po_eta_lemma: "idgen(d) = d \<Longrightarrow> d = lam x. ?f(x)"
+schematic_goal po_eta_lemma: "idgen(d) = d \<Longrightarrow> d = lam x. ?f(x)"
   apply (unfold idgen_def)
   apply (erule sym)
   done
 
 lemma lemma1: