| author | Cezary Kaliszyk <kaliszyk@in.tum.de> | 
| Wed, 27 Jan 2010 13:32:28 +0100 | |
| changeset 961 | 0f88e04eb486 | 
| parent 960 | d7ec7b1204a5 | 
| child 962 | 8a16d6c45720 | 
--- a/Quot/Nominal/Test.thy Wed Jan 27 12:21:40 2010 +0100 +++ b/Quot/Nominal/Test.thy Wed Jan 27 13:32:28 2010 +0100 @@ -202,11 +202,11 @@ bi::"bp \<Rightarrow> name set" where "bi (BP x t) = {x}" - +print_theorems text {* examples 2 *} nominal_datatype trm = - Var "string" + Var "name" | App "trm" "trm" | Lam x::"name" t::"trm" bindset x in t | Let p::"pat" "trm" t::"trm" bind "f p" in t @@ -248,4 +248,4 @@ -end \ No newline at end of file +end