src/HOL/Bali/Name.thy
changeset 37956 ee939247b2fb
parent 35431 8758fe1fc9f8
child 38540 8c08631cb4b6
--- a/src/HOL/Bali/Name.thy	Mon Jul 26 13:50:52 2010 +0200
+++ b/src/HOL/Bali/Name.thy	Mon Jul 26 17:41:26 2010 +0200
@@ -68,14 +68,14 @@
 begin
 
 definition
-  tname_tname_def: "tname (t::tname) \<equiv> t"
+  tname_tname_def: "tname (t::tname) = t"
 
 instance ..
 
 end
 
 definition
-  qtname_qtname_def: "qtname (q::'a qtname_ext_type) \<equiv> q"
+  qtname_qtname_def: "qtname (q::'a qtname_ext_type) = q"
 
 translations
   (type) "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
@@ -84,16 +84,17 @@
 
 axiomatization java_lang::pname --{* package java.lang *}
 
-consts 
+definition
   Object :: qtname
-  SXcpt  :: "xname \<Rightarrow> qtname"
-defs
-  Object_def: "Object  \<equiv> \<lparr>pid = java_lang, tid = Object'\<rparr>"
-  SXcpt_def:  "SXcpt   \<equiv> \<lambda>x.  \<lparr>pid = java_lang, tid = SXcpt' x\<rparr>"
+  where "Object = \<lparr>pid = java_lang, tid = Object'\<rparr>"
+
+definition SXcpt :: "xname \<Rightarrow> qtname"
+  where "SXcpt = (\<lambda>x.  \<lparr>pid = java_lang, tid = SXcpt' x\<rparr>)"
 
 lemma Object_neq_SXcpt [simp]: "Object \<noteq> SXcpt xn"
 by (simp add: Object_def SXcpt_def)
 
 lemma SXcpt_inject [simp]: "(SXcpt xn = SXcpt xm) = (xn = xm)"
 by (simp add: SXcpt_def)
+
 end