--- a/src/HOL/MicroJava/J/TypeRel.thy Mon Jun 11 19:21:13 2001 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy Tue Jun 12 14:11:00 2001 +0200
@@ -13,17 +13,17 @@
widen :: "'c prog => (ty \<times> ty ) set" (* widening *)
cast :: "'c prog => (cname \<times> cname) set" (* casting *)
-syntax
+syntax (xsymbols)
subcls1 :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<prec>C1 _" [71,71,71] 70)
- subcls :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>C _" [71,71,71] 70)
- widen :: "'c prog => [ty , ty ] => bool" ("_ \<turnstile> _ \<preceq> _" [71,71,71] 70)
- cast :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>? _" [71,71,71] 70)
+ subcls :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>C _" [71,71,71] 70)
+ widen :: "'c prog => [ty , ty ] => bool" ("_ \<turnstile> _ \<preceq> _" [71,71,71] 70)
+ cast :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>? _" [71,71,71] 70)
-syntax (HTML)
+syntax
subcls1 :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C1 _" [71,71,71] 70)
- subcls :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C _" [71,71,71] 70)
- widen :: "'c prog => [ty , ty ] => bool" ("_ |- _ <= _" [71,71,71] 70)
- cast :: "'c prog => [cname, cname] => bool" ("_ |- _ <=? _" [71,71,71] 70)
+ subcls :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C _" [71,71,71] 70)
+ widen :: "'c prog => [ty , ty ] => bool" ("_ |- _ <= _" [71,71,71] 70)
+ cast :: "'c prog => [cname, cname] => bool" ("_ |- _ <=? _" [71,71,71] 70)
translations
"G\<turnstile>C \<prec>C1 D" == "(C,D) \<in> subcls1 G"