--- a/src/FOL/ex/LocaleTest.thy Mon Jul 23 13:47:48 2007 +0200
+++ b/src/FOL/ex/LocaleTest.thy Mon Jul 23 13:48:30 2007 +0200
@@ -798,6 +798,9 @@
text {* Naming convention for global objects: prefixes D and d *}
+
+subsection {* Simple examples *}
+
locale Da = fixes a :: o
assumes true: a
@@ -807,7 +810,7 @@
apply simp apply (rule true) done
interpretation D1: Da ["True"]
- where "~ True" = "False"
+ where "~ True == False"
apply -
apply unfold_locales [1] apply rule
by simp
@@ -816,7 +819,7 @@
lemma "False <-> False" apply (rule D1.not_false) done
interpretation D2: Da ["x | ~ x"]
- where "~ (x | ~ x)" = "~ x & x"
+ where "~ (x | ~ x) <-> ~ x & x"
apply -
apply unfold_locales [1] apply fast
by simp