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/SFT/LambdaTerms.thy
changeset 3235 5ebd327ffb96
parent 3088 5e74bd87bcda
child 3236 e2da10806a34 
--- a/Nominal/Ex/SFT/LambdaTerms.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/SFT/LambdaTerms.thy	Mon May 19 12:45:26 2014 +0100
@@ -16,7 +16,7 @@
   App (infixl "\<cdot>" 98) and
   Lam ("\<integral> _. _" [97, 97] 99)
 
-nominal_primrec
+nominal_function
   subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [90, 90, 90] 90)
 where
   "(Var x)[y ::= s] = (if x = y then s else (Var x))"
nominal2