--- 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))"
--- 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
--- 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))"
--- 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)
--- 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"
--- 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 {*
--- 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)}"