changeset 28235 | 89e4d2232ed2 |
parent 28085 | 914183e229e9 |
child 28611 | 983c1855a7af |
--- a/src/FOL/ex/LocaleTest.thy Tue Sep 16 12:25:26 2008 +0200 +++ b/src/FOL/ex/LocaleTest.thy Tue Sep 16 12:26:15 2008 +0200 @@ -97,8 +97,10 @@ locale IB = fixes b assumes asm_B [simp]: "b = b" -locale IC = IA + IB + assumes asm_C: "c = c" - (* TODO: independent type var in c, prohibit locale declaration *) +locale IC = IA + IB + assumes asm_C: "b = b" + +locale IC' = IA + IB + assumes asm_C: "c = c" + (* independent type var in c *) locale ID = IA + IB + fixes d defines def_D: "d == (a = b)"