
diff -r 34b51f436e92 -r ba8c284d4725 src/HOL/Bali/TypeRel.thy
--- a/src/HOL/Bali/TypeRel.thy	Wed Dec 30 19:41:48 2015 +0100
+++ b/src/HOL/Bali/TypeRel.thy	Wed Dec 30 19:57:37 2015 +0100
@@ -38,21 +38,21 @@
 
 
 abbreviation
-  subint1_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<:I1_" [71,71,71] 70)
-  where "G|-I <:I1 J == (I,J) \<in> subint1 G"
+  subint1_syntax :: "prog => [qtname, qtname] => bool" ("_\<turnstile>_\<prec>I1_"  [71,71,71] 70)
+  where "G\<turnstile>I \<prec>I1 J == (I,J) \<in> subint1 G"
 
 abbreviation
-  subint_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<=:I _"[71,71,71] 70)
-  where "G|-I <=:I J == (I,J) \<in>(subint1 G)^*" --{* cf. 9.1.3 *}
+  subint_syntax :: "prog => [qtname, qtname] => bool" ("_\<turnstile>_\<preceq>I _"  [71,71,71] 70)
+  where "G\<turnstile>I \<preceq>I J == (I,J) \<in>(subint1 G)^*" --{* cf. 9.1.3 *}
 
 abbreviation
-  implmt1_syntax :: "prog => [qtname, qtname] => bool" ("_|-_~>1_"  [71,71,71] 70)
-  where "G|-C ~>1 I == (C,I) \<in> implmt1 G"
+  implmt1_syntax :: "prog => [qtname, qtname] => bool" ("_\<turnstile>_\<leadsto>1_"  [71,71,71] 70)
+  where "G\<turnstile>C \<leadsto>1 I == (C,I) \<in> implmt1 G"
 
-notation (xsymbols)
-  subint1_syntax  ("_\<turnstile>_\<prec>I1_"  [71,71,71] 70) and
-  subint_syntax  ("_\<turnstile>_\<preceq>I _"  [71,71,71] 70) and
-  implmt1_syntax   ("_\<turnstile>_\<leadsto>1_"  [71,71,71] 70)
+notation (ASCII)
+  subint1_syntax  ("_|-_<:I1_" [71,71,71] 70) and
+  subint_syntax  ("_|-_<=:I _"[71,71,71] 70) and
+  implmt1_syntax   ("_|-_~>1_"  [71,71,71] 70)
 
 
 subsubsection "subclass and subinterface relations"




