changeset 961 | 0f88e04eb486 |
parent 954 | c009d2535896 |
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