src/HOL/MicroJava/J/TypeRel.thy
changeset 62042 6c6ccf573479
parent 61361 8b5f00202e1a
child 62145 5b946c81dfbf
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Sat Jan 02 18:46:36 2016 +0100
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Sat Jan 02 18:48:45 2016 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  imports Decl
     1.5  begin
     1.6  
     1.7 --- "direct subclass, cf. 8.1.3"
     1.8 +\<comment> "direct subclass, cf. 8.1.3"
     1.9  
    1.10  inductive_set
    1.11    subcls1 :: "'c prog => (cname \<times> cname) set"
    1.12 @@ -181,7 +181,7 @@
    1.13    field  :: "'c prog \<times> cname => ( vname \<rightharpoonup> cname \<times> ty     )" (* ###curry *)
    1.14    fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list" (* ###curry *)
    1.15  
    1.16 --- "methods of a class, with inheritance, overriding and hiding, cf. 8.4.6"
    1.17 +\<comment> "methods of a class, with inheritance, overriding and hiding, cf. 8.4.6"
    1.18  defs method_def [code]: "method \<equiv> \<lambda>(G,C). class_rec G C empty (\<lambda>C fs ms ts.
    1.19                             ts ++ map_of (map (\<lambda>(s,m). (s,(C,m))) ms))"
    1.20  
    1.21 @@ -195,7 +195,7 @@
    1.22  done
    1.23  
    1.24  
    1.25 --- "list of fields of a class, including inherited and hidden ones"
    1.26 +\<comment> "list of fields of a class, including inherited and hidden ones"
    1.27  defs fields_def [code]: "fields \<equiv> \<lambda>(G,C). class_rec G C []    (\<lambda>C fs ms ts.
    1.28                             map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ ts)"
    1.29  
    1.30 @@ -219,12 +219,12 @@
    1.31  done
    1.32  
    1.33  
    1.34 --- "widening, viz. method invocation conversion,cf. 5.3 i.e. sort of syntactic subtyping"
    1.35 +\<comment> "widening, viz. method invocation conversion,cf. 5.3 i.e. sort of syntactic subtyping"
    1.36  inductive
    1.37    widen   :: "'c prog => [ty   , ty   ] => bool" ("_ \<turnstile> _ \<preceq> _"   [71,71,71] 70)
    1.38    for G :: "'c prog"
    1.39  where
    1.40 -  refl   [intro!, simp]:       "G\<turnstile>      T \<preceq> T"   -- "identity conv., cf. 5.1.1"
    1.41 +  refl   [intro!, simp]:       "G\<turnstile>      T \<preceq> T"   \<comment> "identity conv., cf. 5.1.1"
    1.42  | subcls         : "G\<turnstile>C\<preceq>C D ==> G\<turnstile>Class C \<preceq> Class D"
    1.43  | null   [intro!]:             "G\<turnstile>     NT \<preceq> RefT R"
    1.44  
    1.45 @@ -232,8 +232,8 @@
    1.46  
    1.47  lemmas refl = HOL.refl
    1.48  
    1.49 --- "casting conversion, cf. 5.5 / 5.1.5"
    1.50 --- "left out casts on primitve types"
    1.51 +\<comment> "casting conversion, cf. 5.5 / 5.1.5"
    1.52 +\<comment> "left out casts on primitve types"
    1.53  inductive
    1.54    cast    :: "'c prog => [ty   , ty   ] => bool" ("_ \<turnstile> _ \<preceq>? _"  [71,71,71] 70)
    1.55    for G :: "'c prog"