Quot/Nominal/Test.thy
changeset 962 8a16d6c45720
parent 961 0f88e04eb486
child 966 8ba35ce16f7e
equal deleted inserted replaced
961:0f88e04eb486 962:8a16d6c45720
   220   "f PN = {}"
   220   "f PN = {}"
   221 | "f (PS x) = {x}"
   221 | "f (PS x) = {x}"
   222 | "f (PD (x,y)) = {x,y}"
   222 | "f (PD (x,y)) = {x,y}"
   223 
   223 
   224 nominal_datatype trm2 =
   224 nominal_datatype trm2 =
   225   Var2 "string"
   225   Var2 "name"
   226 | App2 "trm2" "trm2"
   226 | App2 "trm2" "trm2"
   227 | Lam2 x::"name" t::"trm2"          bindset x in t 
   227 | Lam2 x::"name" t::"trm2"          bindset x in t 
   228 | Let2 p::"pat2" "trm2" t::"trm2"   bind "f2 p" in t
   228 | Let2 p::"pat2" "trm2" t::"trm2"   bind "f2 p" in t
   229 and pat2 =
   229 and pat2 =
   230   PN2
   230   PN2