src/HOL/Bali/TypeRel.thy
changeset 14674 3506a9af46fc
parent 13688 a0b16d42d489
child 14700 2f885b7e5ba7
--- a/src/HOL/Bali/TypeRel.thy	Mon Apr 26 14:54:45 2004 +0200
+++ b/src/HOL/Bali/TypeRel.thy	Mon Apr 26 14:56:18 2004 +0200
@@ -29,16 +29,16 @@
 
 consts
 
-(*subint1, in Decl.thy*)                     (* direct subinterface       *)
-(*subint , by translation*)                  (* subinterface (+ identity) *)
-(*subcls1, in Decl.thy*)                     (* direct subclass           *)
-(*subcls , by translation*)                  (*        subclass           *)
-(*subclseq, by translation*)                 (* subclass + identity       *)
+(*subint1, in Decl.thy*)                     (* direct subinterface       *)
+(*subint , by translation*)                  (* subinterface (+ identity) *)
+(*subcls1, in Decl.thy*)                     (* direct subclass           *)
+(*subcls , by translation*)                  (*        subclass           *)
+(*subclseq, by translation*)                 (* subclass + identity       *)
   implmt1   :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct implementation *}
-  implmt    :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{*        implementation *}
+  implmt    :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{*        implementation *}
   widen     :: "prog \<Rightarrow> (ty    \<times> ty   ) set" --{*        widening       *}
   narrow    :: "prog \<Rightarrow> (ty    \<times> ty   ) set" --{*        narrowing      *}
-  cast     :: "prog \<Rightarrow> (ty    \<times> ty   ) set"  --{*        casting        *}
+  cast     :: "prog \<Rightarrow> (ty    \<times> ty   ) set"  --{*        casting        *}
 
 syntax