# HG changeset patch
# User ballarin
# Date 1157376450 -7200
# Node ID bb75c1cdf913a3788e3e337cc326a552c6c73245
# Parent  0bda06d731ee73d4b805e2762e5143c5590d43ea
More locale test code.

diff -r 0bda06d731ee -r bb75c1cdf913 src/FOL/ex/LocaleTest.thy
--- a/src/FOL/ex/LocaleTest.thy	Mon Sep 04 15:27:00 2006 +0200
+++ b/src/FOL/ex/LocaleTest.thy	Mon Sep 04 15:27:30 2006 +0200
@@ -780,4 +780,18 @@
   shows "(x +++ y) +++ z = x +++ (y +++ z)"
   apply (rule r_assoc) done
 
+
+subsection {* Import of Locales with Predicates as Interpretation *}
+
+locale Ra =
+  assumes Ra: "True"
+
+locale Rb = Ra +
+  assumes Rb: "True"
+
+locale Rc = Rb +
+  assumes Rc: "True"
+
+print_locale! Rc
+
 end