equal
deleted
inserted
replaced
95 |
95 |
96 locale IA = fixes a assumes asm_A: "a = a" |
96 locale IA = fixes a assumes asm_A: "a = a" |
97 |
97 |
98 locale IB = fixes b assumes asm_B [simp]: "b = b" |
98 locale IB = fixes b assumes asm_B [simp]: "b = b" |
99 |
99 |
100 locale IC = IA + IB + assumes asm_C: "c = c" |
100 locale IC = IA + IB + assumes asm_C: "b = b" |
101 (* TODO: independent type var in c, prohibit locale declaration *) |
101 |
|
102 locale IC' = IA + IB + assumes asm_C: "c = c" |
|
103 (* independent type var in c *) |
102 |
104 |
103 locale ID = IA + IB + fixes d defines def_D: "d == (a = b)" |
105 locale ID = IA + IB + fixes d defines def_D: "d == (a = b)" |
104 |
106 |
105 theorem (in ID) True .. |
107 theorem (in ID) True .. |
106 |
108 |