equal
deleted
inserted
replaced
5 |
5 |
6 atom_decl name |
6 atom_decl name |
7 |
7 |
8 nominal_datatype lt = |
8 nominal_datatype lt = |
9 Var name ("_~" [150] 149) |
9 Var name ("_~" [150] 149) |
10 | Abs x::"name" t::"lt" bind x in t |
10 | Abs x::"name" t::"lt" binds x in t |
11 | App lt lt (infixl "$" 100) |
11 | App lt lt (infixl "$" 100) |
12 |
12 |
13 nominal_primrec |
13 nominal_primrec |
14 subst :: "lt \<Rightarrow> lt \<Rightarrow> name \<Rightarrow> lt" ("_[_'/_]" [200,0,0] 190) |
14 subst :: "lt \<Rightarrow> lt \<Rightarrow> name \<Rightarrow> lt" ("_[_'/_]" [200,0,0] 190) |
15 where |
15 where |