# HG changeset patch
# User wenzelm
# Date 1326554062 -3600
# Node ID d86ef6b960973ae007a2849e2c5f86e2f0cf881c
# Parent  2616e68877c9516d18f512d2618d9026de8e9c8b
tuned white space;

diff -r 2616e68877c9 -r d86ef6b96097 src/HOL/Bali/Conform.thy
--- a/src/HOL/Bali/Conform.thy	Sat Jan 14 16:12:09 2012 +0100
+++ b/src/HOL/Bali/Conform.thy	Sat Jan 14 16:14:22 2012 +0100
@@ -380,8 +380,7 @@
   conforms :: "state \<Rightarrow> env' \<Rightarrow> bool"  ("_\<Colon>\<preceq>_" [71,71] 70)  where
    "xs\<Colon>\<preceq>E =
       (let (G, L) = E; s = snd xs; l = locals s in
-        (\<forall>r. \<forall>obj\<in>globs s r:           G,s\<turnstile>obj   \<Colon>\<preceq>\<surd>r) \<and>
-                    \<spacespace>                   G,s\<turnstile>l    [\<sim>\<Colon>\<preceq>]L\<spacespace> \<and>
+        (\<forall>r. \<forall>obj\<in>globs s r: G,s\<turnstile>obj \<Colon>\<preceq>\<surd>r) \<and> G,s\<turnstile>l [\<sim>\<Colon>\<preceq>]L \<and>
         (\<forall>a. fst xs=Some(Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)) \<and>
              (fst xs=Some(Jump Ret) \<longrightarrow> l Result \<noteq> None))"
 
diff -r 2616e68877c9 -r d86ef6b96097 src/HOL/Bali/Decl.thy
--- a/src/HOL/Bali/Decl.thy	Sat Jan 14 16:12:09 2012 +0100
+++ b/src/HOL/Bali/Decl.thy	Sat Jan 14 16:14:22 2012 +0100
@@ -70,7 +70,7 @@
   fix x y z::acc_modi
   show "(x < y) = (x \<le> y \<and> \<not> y \<le> x)"
     by (auto simp add: le_acc_def less_acc_def split add: acc_modi.split) 
-  show "x \<le> x"               \<spacespace>\<spacespace>    -- reflexivity
+  show "x \<le> x"                       -- reflexivity
     by (auto simp add: le_acc_def)
   {
     assume "x \<le> y" "y \<le> z"           -- transitivity 
@@ -766,8 +766,7 @@
 
 section "general recursion operators for the interface and class hiearchies"
 
-function
-  iface_rec  :: "prog \<Rightarrow> qtname \<Rightarrow>   \<spacespace>(qtname \<Rightarrow> iface \<Rightarrow> 'a set \<Rightarrow> 'a) \<Rightarrow> 'a"
+function iface_rec  :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<Rightarrow> iface \<Rightarrow> 'a set \<Rightarrow> 'a) \<Rightarrow> 'a"
 where
 [simp del]: "iface_rec G I f = 
   (case iface G I of 
diff -r 2616e68877c9 -r d86ef6b96097 src/HOL/Bali/Example.thy
--- a/src/HOL/Bali/Example.thy	Sat Jan 14 16:12:09 2012 +0100
+++ b/src/HOL/Bali/Example.thy	Sat Jan 14 16:14:22 2012 +0100
@@ -275,8 +275,8 @@
 definition
   test :: "(ty)list \<Rightarrow> stmt" where
   "test pTs = (e:==NewC Ext;; 
-           \<spacespace> Try Expr({Main,ClassT Base,IntVir}!!e\<cdot>foo({pTs}[Lit Null]))
-           \<spacespace> Catch((SXcpt NullPointer) z)
+           Try Expr({Main,ClassT Base,IntVir}!!e\<cdot>foo({pTs}[Lit Null]))
+           Catch((SXcpt NullPointer) z)
            (lab1\<bullet> While(Acc 
                         (Acc (arr_viewed_from Main Ext).[Lit (Intg 2)])) Skip))"
 
diff -r 2616e68877c9 -r d86ef6b96097 src/HOL/Bali/Table.thy
--- a/src/HOL/Bali/Table.thy	Sat Jan 14 16:12:09 2012 +0100
+++ b/src/HOL/Bali/Table.thy	Sat Jan 14 16:14:22 2012 +0100
@@ -280,9 +280,8 @@
 done
 
 
-definition
-  Un_tables :: "('a, 'b) tables set \<Rightarrow> ('a, 'b) tables"
-  where "Un_tables ts\<spacespace>\<spacespace>= (\<lambda>k. \<Union>t\<in>ts. t k)"
+definition Un_tables :: "('a, 'b) tables set \<Rightarrow> ('a, 'b) tables"
+  where "Un_tables ts = (\<lambda>k. \<Union>t\<in>ts. t k)"
 
 definition
   overrides_t :: "('a, 'b) tables \<Rightarrow> ('a, 'b) tables \<Rightarrow> ('a, 'b) tables"  (infixl "\<oplus>\<oplus>" 100)
diff -r 2616e68877c9 -r d86ef6b96097 src/HOL/Bali/TypeRel.thy
--- a/src/HOL/Bali/TypeRel.thy	Sat Jan 14 16:12:09 2012 +0100
+++ b/src/HOL/Bali/TypeRel.thy	Sat Jan 14 16:14:22 2012 +0100
@@ -337,9 +337,9 @@
   implmt :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile>_\<leadsto>_" [71,71,71] 70)
   for G :: prog
 where
-  direct:         "G\<turnstile>C\<leadsto>1J     \<spacespace>\<spacespace>     \<Longrightarrow> G\<turnstile>C\<leadsto>J"
-| subint:        "\<lbrakk>G\<turnstile>C\<leadsto>1I; G\<turnstile>I\<preceq>I J\<rbrakk>  \<Longrightarrow> G\<turnstile>C\<leadsto>J"
-| subcls1:       "\<lbrakk>G\<turnstile>C\<prec>\<^sub>C1D; G\<turnstile>D\<leadsto>J \<rbrakk>  \<Longrightarrow> G\<turnstile>C\<leadsto>J"
+  direct: "G\<turnstile>C\<leadsto>1J \<Longrightarrow> G\<turnstile>C\<leadsto>J"
+| subint: "G\<turnstile>C\<leadsto>1I \<Longrightarrow> G\<turnstile>I\<preceq>I J \<Longrightarrow> G\<turnstile>C\<leadsto>J"
+| subcls1: "G\<turnstile>C\<prec>\<^sub>C1D \<Longrightarrow> G\<turnstile>D\<leadsto>J \<Longrightarrow> G\<turnstile>C\<leadsto>J"
 
 lemma implmtD: "G\<turnstile>C\<leadsto>J \<Longrightarrow> (\<exists>I. G\<turnstile>C\<leadsto>1I \<and> G\<turnstile>I\<preceq>I J) \<or> (\<exists>D. G\<turnstile>C\<prec>\<^sub>C1D \<and> G\<turnstile>D\<leadsto>J)" 
 apply (erule implmt.induct)
@@ -602,9 +602,9 @@
 | obj_arr: "G\<turnstile>Class Object\<succ>T.[]"
 | int_cls: "G\<turnstile>     Iface I\<succ>Class C"
 | subint:  "imethds G I hidings imethds G J entails 
-           (\<lambda>(md, mh   ) (md',mh').\<spacespace>G\<turnstile>mrt mh\<preceq>mrt mh') \<Longrightarrow>
-           \<not>G\<turnstile>I\<preceq>I J         \<spacespace>\<spacespace>\<spacespace>\<Longrightarrow> G\<turnstile>     Iface I\<succ>Iface J"
-| array:   "G\<turnstile>RefT S\<succ>RefT T   \<spacespace>\<Longrightarrow> G\<turnstile>   RefT S.[]\<succ>RefT T.[]"
+           (\<lambda>(md, mh   ) (md',mh'). G\<turnstile>mrt mh\<preceq>mrt mh') \<Longrightarrow>
+           \<not>G\<turnstile>I\<preceq>I J         \<Longrightarrow> G\<turnstile>     Iface I\<succ>Iface J"
+| array:   "G\<turnstile>RefT S\<succ>RefT T \<Longrightarrow> G\<turnstile>   RefT S.[]\<succ>RefT T.[]"
 
 (*unused*)
 lemma narrow_RefT: "G\<turnstile>RefT R\<succ>T \<Longrightarrow> \<exists>t. T=RefT t"
diff -r 2616e68877c9 -r d86ef6b96097 src/HOL/Bali/WellForm.thy
--- a/src/HOL/Bali/WellForm.thy	Sat Jan 14 16:12:09 2012 +0100
+++ b/src/HOL/Bali/WellForm.thy	Sat Jan 14 16:14:22 2012 +0100
@@ -58,9 +58,9 @@
 definition
   wf_mhead :: "prog \<Rightarrow> pname \<Rightarrow> sig \<Rightarrow> mhead \<Rightarrow> bool" where
   "wf_mhead G P = (\<lambda> sig mh. length (parTs sig) = length (pars mh) \<and>
-                            \<spacespace> ( \<forall>T\<in>set (parTs sig). is_acc_type G P T) \<and> 
+                            ( \<forall>T\<in>set (parTs sig). is_acc_type G P T) \<and> 
                             is_acc_type G P (resTy mh) \<and>
-                            \<spacespace> distinct (pars mh))"
+                            distinct (pars mh))"
 
 
 text {*
diff -r 2616e68877c9 -r d86ef6b96097 src/HOL/Bali/WellType.thy
--- a/src/HOL/Bali/WellType.thy	Sat Jan 14 16:12:09 2012 +0100
+++ b/src/HOL/Bali/WellType.thy	Sat Jan 14 16:14:22 2012 +0100
@@ -108,7 +108,7 @@
 
 definition
   --{* applicable methods, cf. 15.11.2.1 *}
-  appl_methds :: "prog \<Rightarrow> qtname \<Rightarrow>  ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" where
+  appl_methds :: "prog \<Rightarrow> qtname \<Rightarrow>  ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list) set" where
   "appl_methds G S rt = (\<lambda> sig. 
       {(mh,pTs') |mh pTs'. mh \<in> mheads G S rt \<lparr>name=name sig,parTs=pTs'\<rparr> \<and> 
                            G\<turnstile>(parTs sig)[\<preceq>]pTs'})"
@@ -121,7 +121,7 @@
 
 definition
   --{* maximally specific methods, cf. 15.11.2.2 *}
-  max_spec :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" where
+  max_spec :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list) set" where
   "max_spec G S rt sig = {m. m \<in>appl_methds G S rt sig \<and>
                           (\<forall>m'\<in>appl_methds G S rt sig. more_spec G m' m \<longrightarrow> m'=m)}"