author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
Wed, 03 Feb 2010 12:34:53 +0100 | |
changeset 1042 | 5a3bc323661c |
parent 1041 | 21c2936190c7 |
child 1044 | ef024a42c1bb |
--- a/Quot/Nominal/Terms.thy Wed Feb 03 12:34:01 2010 +0100 +++ b/Quot/Nominal/Terms.thy Wed Feb 03 12:34:53 2010 +0100 @@ -646,7 +646,7 @@ quotient_type qtrm4 = trm4 / alpha4 and qtrm4list = "trm4 list" / alpha4list - by (simp_all add: alpha4_equivp alpha4list_equivp + by (simp_all add: alpha4_equivp alpha4list_equivp) datatype rtrm5 =