Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
No interpretation of locale with dangling type frees.
authorballarin
Tue, 16 Sep 2008 12:26:15 +0200
changeset 28235 89e4d2232ed2
parent 28234 fc420a5cf72e
child 28236 c447b60d67f5
No interpretation of locale with dangling type frees.
src/FOL/ex/LocaleTest.thy file | annotate | diff | comparison | revisions 
--- 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)"
isabelle