src/HOL/MicroJava/J/TypeRel.thy
changeset 11372 648795477bb5
parent 11284 981ea92a86dd
child 11987 bf31b35949ce
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Mon Jun 11 19:21:13 2001 +0200
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Tue Jun 12 14:11:00 2001 +0200
     1.3 @@ -13,17 +13,17 @@
     1.4    widen   :: "'c prog => (ty    \<times> ty   ) set"  (* widening *)
     1.5    cast    :: "'c prog => (cname \<times> cname) set"  (* casting *)
     1.6  
     1.7 -syntax
     1.8 +syntax (xsymbols)
     1.9    subcls1 :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<prec>C1 _" [71,71,71] 70)
    1.10 -  subcls  :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>C _" [71,71,71] 70)
    1.11 -  widen   :: "'c prog => [ty   , ty   ] => bool" ("_ \<turnstile> _ \<preceq> _" [71,71,71] 70)
    1.12 -  cast    :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>? _" [71,71,71] 70)
    1.13 +  subcls  :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>C _"  [71,71,71] 70)
    1.14 +  widen   :: "'c prog => [ty   , ty   ] => bool" ("_ \<turnstile> _ \<preceq> _"   [71,71,71] 70)
    1.15 +  cast    :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>? _"  [71,71,71] 70)
    1.16  
    1.17 -syntax (HTML)
    1.18 +syntax
    1.19    subcls1 :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C1 _" [71,71,71] 70)
    1.20 -  subcls  :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C _" [71,71,71] 70)
    1.21 -  widen   :: "'c prog => [ty   , ty   ] => bool" ("_ |- _ <= _" [71,71,71] 70)
    1.22 -  cast    :: "'c prog => [cname, cname] => bool" ("_ |- _ <=? _" [71,71,71] 70)
    1.23 +  subcls  :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C _"  [71,71,71] 70)
    1.24 +  widen   :: "'c prog => [ty   , ty   ] => bool" ("_ |- _ <= _"   [71,71,71] 70)
    1.25 +  cast    :: "'c prog => [cname, cname] => bool" ("_ |- _ <=? _"  [71,71,71] 70)
    1.26  
    1.27  translations
    1.28    "G\<turnstile>C \<prec>C1 D" == "(C,D) \<in> subcls1 G"