Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/CCL/Fix.thy
changeset 61337 4645502c3c64
parent 60770 240563fbf41d 
--- a/src/CCL/Fix.thy	Tue Oct 06 13:31:44 2015 +0200
+++ b/src/CCL/Fix.thy	Tue Oct 06 15:14:28 2015 +0200
@@ -93,7 +93,7 @@
 
 (* 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)
@@ -125,7 +125,7 @@
   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
isabelle