Mercurial Mercurial > hg > nominal2 / 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.
Nominal/Ex/LetRecFunNo.thy
changeset 3235 5ebd327ffb96
parent 3150 7ad3b1421b82
child 3236 e2da10806a34 
--- a/Nominal/Ex/LetRecFunNo.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/LetRecFunNo.thy	Mon May 19 12:45:26 2014 +0100
@@ -17,7 +17,7 @@
   "bn ANil = []"
 | "bn (ACons x t as) = (atom x) # (bn as)"
 
-nominal_primrec substrec where
+nominal_function substrec where
   "substrec fa fl fd y z (Var x) = (if (y = x) then z else (Var x))"
 | "substrec fa fl fd y z (App l r) = fa l r"
 | "(set (bn as) \<sharp>* (Let as t, y, z) \<and> (\<forall>bs s. set (bn bs) \<sharp>* (Let bs s, y, z) \<longrightarrow> Let as t = Let bs s \<longrightarrow> fl as t = fl bs s)) \<Longrightarrow>
@@ -55,7 +55,7 @@
   done
 termination (eqvt) by lexicographic_order
 
-nominal_primrec substarec :: "(name \<Rightarrow> trm \<Rightarrow> assn \<Rightarrow> assn) \<Rightarrow> assn \<Rightarrow> assn" where
+nominal_function substarec :: "(name \<Rightarrow> trm \<Rightarrow> assn \<Rightarrow> assn) \<Rightarrow> assn \<Rightarrow> assn" where
   "substarec fac ANil = ANil"
 | "substarec fac (ACons x t as) = fac x t as"
   unfolding eqvt_def substarec_graph_def
nominal2