src/HOL/Bali/Name.thy
changeset 37956 ee939247b2fb
parent 35431 8758fe1fc9f8
child 38540 8c08631cb4b6
     1.1 --- a/src/HOL/Bali/Name.thy	Mon Jul 26 13:50:52 2010 +0200
     1.2 +++ b/src/HOL/Bali/Name.thy	Mon Jul 26 17:41:26 2010 +0200
     1.3 @@ -68,14 +68,14 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  tname_tname_def: "tname (t::tname) \<equiv> t"
     1.8 +  tname_tname_def: "tname (t::tname) = t"
     1.9  
    1.10  instance ..
    1.11  
    1.12  end
    1.13  
    1.14  definition
    1.15 -  qtname_qtname_def: "qtname (q::'a qtname_ext_type) \<equiv> q"
    1.16 +  qtname_qtname_def: "qtname (q::'a qtname_ext_type) = q"
    1.17  
    1.18  translations
    1.19    (type) "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
    1.20 @@ -84,16 +84,17 @@
    1.21  
    1.22  axiomatization java_lang::pname --{* package java.lang *}
    1.23  
    1.24 -consts 
    1.25 +definition
    1.26    Object :: qtname
    1.27 -  SXcpt  :: "xname \<Rightarrow> qtname"
    1.28 -defs
    1.29 -  Object_def: "Object  \<equiv> \<lparr>pid = java_lang, tid = Object'\<rparr>"
    1.30 -  SXcpt_def:  "SXcpt   \<equiv> \<lambda>x.  \<lparr>pid = java_lang, tid = SXcpt' x\<rparr>"
    1.31 +  where "Object = \<lparr>pid = java_lang, tid = Object'\<rparr>"
    1.32 +
    1.33 +definition SXcpt :: "xname \<Rightarrow> qtname"
    1.34 +  where "SXcpt = (\<lambda>x.  \<lparr>pid = java_lang, tid = SXcpt' x\<rparr>)"
    1.35  
    1.36  lemma Object_neq_SXcpt [simp]: "Object \<noteq> SXcpt xn"
    1.37  by (simp add: Object_def SXcpt_def)
    1.38  
    1.39  lemma SXcpt_inject [simp]: "(SXcpt xn = SXcpt xm) = (xn = xm)"
    1.40  by (simp add: SXcpt_def)
    1.41 +
    1.42  end