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