src/HOL/Bali/TypeRel.thy
changeset 35067 af4c18c30593
parent 32960 69916a850301
child 35069 09154b995ed8
--- a/src/HOL/Bali/TypeRel.thy	Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/TypeRel.thy	Wed Feb 10 00:45:16 2010 +0100
@@ -35,37 +35,22 @@
 (*subclseq, by translation*)                 (* subclass + identity       *)
   implmt1   :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct implementation *}
 
-syntax
+abbreviation
+  subint1_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<:I1_" [71,71,71] 70)
+  where "G|-I <:I1 J == (I,J) \<in> subint1 G"
 
- "_subint1" :: "prog => [qtname, qtname] => bool" ("_|-_<:I1_" [71,71,71] 70)
- "_subint"  :: "prog => [qtname, qtname] => bool" ("_|-_<=:I _"[71,71,71] 70)
- (* Defined in Decl.thy:
- "_subcls1" :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70)
- "_subclseq":: "prog => [qtname, qtname] => bool" ("_|-_<=:C _"[71,71,71] 70)
- "_subcls"  :: "prog => [qtname, qtname] => bool" ("_|-_<:C _"[71,71,71] 70)
- *)
- "@implmt1" :: "prog => [qtname, qtname] => bool" ("_|-_~>1_"  [71,71,71] 70)
-
-syntax (xsymbols)
+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 *}
 
-  "_subint1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>I1_"  [71,71,71] 70)
-  "_subint"  :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>I _"  [71,71,71] 70)
-  (* Defined in Decl.thy:
-\  "_subcls1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C\<^sub>1_"  [71,71,71] 70)
-  "_subclseq":: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>\<^sub>C _"  [71,71,71] 70)
-  "_subcls"  :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C _"  [71,71,71] 70)
-  *)
-  "_implmt1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<leadsto>1_"  [71,71,71] 70)
+abbreviation
+  implmt1_syntax :: "prog => [qtname, qtname] => bool" ("_|-_~>1_"  [71,71,71] 70)
+  where "G|-C ~>1 I == (C,I) \<in> implmt1 G"
 
-translations
-
-        "G\<turnstile>I \<prec>I1 J" == "(I,J) \<in> subint1 G"
-        "G\<turnstile>I \<preceq>I  J" == "(I,J) \<in>(subint1 G)^*" --{* cf. 9.1.3 *}
-        (* Defined in Decl.thy:
-        "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D" == "(C,D) \<in> subcls1 G"
-        "G\<turnstile>C \<preceq>\<^sub>C  D" == "(C,D) \<in>(subcls1 G)^*" 
-        *)
-        "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)
 
 
 section "subclass and subinterface relations"