# HG changeset patch
# User wenzelm
# Date 1280161519 -7200
# Node ID a79abb22ca9c46a4e7e9d7a8977233255b5b0096
# Parent  d9549f9da77933fb75fd542a0e2c6385d7b2f6ac# Parent  00e848690339ceb039eeb8b3f9ccb4af021f2aa8
merged

diff -r d9549f9da779 -r a79abb22ca9c src/HOL/Bali/AxCompl.thy
--- a/src/HOL/Bali/AxCompl.thy	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/AxCompl.thy	Mon Jul 26 18:25:19 2010 +0200
@@ -20,8 +20,9 @@
            
 section "set of not yet initialzed classes"
 
-definition nyinitcls :: "prog \<Rightarrow> state \<Rightarrow> qtname set" where
- "nyinitcls G s \<equiv> {C. is_class G C \<and> \<not> initd C s}"
+definition
+  nyinitcls :: "prog \<Rightarrow> state \<Rightarrow> qtname set"
+  where "nyinitcls G s = {C. is_class G C \<and> \<not> initd C s}"
 
 lemma nyinitcls_subset_class: "nyinitcls G s \<subseteq> {C. is_class G C}"
 apply (unfold nyinitcls_def)
@@ -113,8 +114,9 @@
 
 section "init-le"
 
-definition init_le :: "prog \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> bool" ("_\<turnstile>init\<le>_"  [51,51] 50) where
- "G\<turnstile>init\<le>n \<equiv> \<lambda>s. card (nyinitcls G s) \<le> n"
+definition
+  init_le :: "prog \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> bool" ("_\<turnstile>init\<le>_"  [51,51] 50)
+  where "G\<turnstile>init\<le>n = (\<lambda>s. card (nyinitcls G s) \<le> n)"
   
 lemma init_le_def2 [simp]: "(G\<turnstile>init\<le>n) s = (card (nyinitcls G s)\<le>n)"
 apply (unfold init_le_def)
@@ -132,27 +134,22 @@
 
 section "Most General Triples and Formulas"
 
-definition remember_init_state :: "state assn" ("\<doteq>") where
-  "\<doteq> \<equiv> \<lambda>Y s Z. s = Z"
+definition
+  remember_init_state :: "state assn" ("\<doteq>")
+  where "\<doteq> \<equiv> \<lambda>Y s Z. s = Z"
 
 lemma remember_init_state_def2 [simp]: "\<doteq> Y = op ="
 apply (unfold remember_init_state_def)
 apply (simp (no_asm))
 done
 
-consts
-  
+definition
   MGF ::"[state assn, term, prog] \<Rightarrow> state triple"   ("{_} _\<succ> {_\<rightarrow>}"[3,65,3]62)
-  MGFn::"[nat       , term, prog] \<Rightarrow> state triple" ("{=:_} _\<succ> {_\<rightarrow>}"[3,65,3]62)
+  where "{P} t\<succ> {G\<rightarrow>} = {P} t\<succ> {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')}"
 
-defs
-  
-
-  MGF_def:
-  "{P} t\<succ> {G\<rightarrow>} \<equiv> {P} t\<succ> {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')}"
-
-  MGFn_def:
-  "{=:n} t\<succ> {G\<rightarrow>} \<equiv> {\<doteq> \<and>. G\<turnstile>init\<le>n} t\<succ> {G\<rightarrow>}"
+definition
+  MGFn :: "[nat, term, prog] \<Rightarrow> state triple" ("{=:_} _\<succ> {_\<rightarrow>}"[3,65,3]62)
+  where "{=:n} t\<succ> {G\<rightarrow>} = {\<doteq> \<and>. G\<turnstile>init\<le>n} t\<succ> {G\<rightarrow>}"
 
 (* unused *)
 lemma MGF_valid: "wf_prog G \<Longrightarrow> G,{}\<Turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
@@ -574,9 +571,9 @@
 unroll the loop in iterated evaluations of the expression and evaluations of
 the loop body. *}
 
-definition unroll :: "prog \<Rightarrow> label \<Rightarrow> expr \<Rightarrow> stmt \<Rightarrow> (state \<times>  state) set" where
-
- "unroll G l e c \<equiv> {(s,t). \<exists> v s1 s2.
+definition
+  unroll :: "prog \<Rightarrow> label \<Rightarrow> expr \<Rightarrow> stmt \<Rightarrow> (state \<times>  state) set" where
+  "unroll G l e c = {(s,t). \<exists> v s1 s2.
                              G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s1 \<and> the_Bool v \<and> normal s1 \<and>
                              G\<turnstile>s1 \<midarrow>c\<rightarrow> s2 \<and> t=(abupd (absorb (Cont l)) s2)}"
 
diff -r d9549f9da779 -r a79abb22ca9c src/HOL/Bali/AxExample.thy
--- a/src/HOL/Bali/AxExample.thy	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/AxExample.thy	Mon Jul 26 18:25:19 2010 +0200
@@ -8,10 +8,11 @@
 imports AxSem Example
 begin
 
-definition arr_inv :: "st \<Rightarrow> bool" where
- "arr_inv \<equiv> \<lambda>s. \<exists>obj a T el. globs s (Stat Base) = Some obj \<and>
+definition
+  arr_inv :: "st \<Rightarrow> bool" where
+ "arr_inv = (\<lambda>s. \<exists>obj a T el. globs s (Stat Base) = Some obj \<and>
                               values obj (Inl (arr, Base)) = Some (Addr a) \<and>
-                              heap s a = Some \<lparr>tag=Arr T 2,values=el\<rparr>"
+                              heap s a = Some \<lparr>tag=Arr T 2,values=el\<rparr>)"
 
 lemma arr_inv_new_obj: 
 "\<And>a. \<lbrakk>arr_inv s; new_Addr (heap s)=Some a\<rbrakk> \<Longrightarrow> arr_inv (gupd(Inl a\<mapsto>x) s)"
diff -r d9549f9da779 -r a79abb22ca9c src/HOL/Bali/AxSem.thy
--- a/src/HOL/Bali/AxSem.thy	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/AxSem.thy	Mon Jul 26 18:25:19 2010 +0200
@@ -62,8 +62,9 @@
 translations
   (type) "'a assn" <= (type) "vals \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
 
-definition assn_imp :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> bool" (infixr "\<Rightarrow>" 25) where
- "P \<Rightarrow> Q \<equiv> \<forall>Y s Z. P Y s Z \<longrightarrow> Q Y s Z"
+definition
+  assn_imp :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> bool" (infixr "\<Rightarrow>" 25)
+  where "(P \<Rightarrow> Q) = (\<forall>Y s Z. P Y s Z \<longrightarrow> Q Y s Z)"
   
 lemma assn_imp_def2 [iff]: "(P \<Rightarrow> Q) = (\<forall>Y s Z. P Y s Z \<longrightarrow> Q Y s Z)"
 apply (unfold assn_imp_def)
@@ -75,8 +76,9 @@
 
 subsection "peek-and"
 
-definition peek_and :: "'a assn \<Rightarrow> (state \<Rightarrow>  bool) \<Rightarrow> 'a assn" (infixl "\<and>." 13) where
- "P \<and>. p \<equiv> \<lambda>Y s Z. P Y s Z \<and> p s"
+definition
+  peek_and :: "'a assn \<Rightarrow> (state \<Rightarrow>  bool) \<Rightarrow> 'a assn" (infixl "\<and>." 13)
+  where "(P \<and>. p) = (\<lambda>Y s Z. P Y s Z \<and> p s)"
 
 lemma peek_and_def2 [simp]: "peek_and P p Y s = (\<lambda>Z. (P Y s Z \<and> p s))"
 apply (unfold peek_and_def)
@@ -114,8 +116,9 @@
 
 subsection "assn-supd"
 
-definition assn_supd :: "'a assn \<Rightarrow> (state \<Rightarrow> state) \<Rightarrow> 'a assn" (infixl ";." 13) where
- "P ;. f \<equiv> \<lambda>Y s' Z. \<exists>s. P Y s Z \<and> s' = f s"
+definition
+  assn_supd :: "'a assn \<Rightarrow> (state \<Rightarrow> state) \<Rightarrow> 'a assn" (infixl ";." 13)
+  where "(P ;. f) = (\<lambda>Y s' Z. \<exists>s. P Y s Z \<and> s' = f s)"
 
 lemma assn_supd_def2 [simp]: "assn_supd P f Y s' Z = (\<exists>s. P Y s Z \<and> s' = f s)"
 apply (unfold assn_supd_def)
@@ -124,8 +127,9 @@
 
 subsection "supd-assn"
 
-definition supd_assn :: "(state \<Rightarrow> state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn" (infixr ".;" 13) where
- "f .; P \<equiv> \<lambda>Y s. P Y (f s)"
+definition
+  supd_assn :: "(state \<Rightarrow> state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn" (infixr ".;" 13)
+  where "(f .; P) = (\<lambda>Y s. P Y (f s))"
 
 
 lemma supd_assn_def2 [simp]: "(f .; P) Y s = P Y (f s)"
@@ -143,8 +147,9 @@
 
 subsection "subst-res"
 
-definition subst_res :: "'a assn \<Rightarrow> res \<Rightarrow> 'a assn" ("_\<leftarrow>_"  [60,61] 60) where
- "P\<leftarrow>w \<equiv> \<lambda>Y. P w"
+definition
+  subst_res :: "'a assn \<Rightarrow> res \<Rightarrow> 'a assn" ("_\<leftarrow>_"  [60,61] 60)
+  where "P\<leftarrow>w = (\<lambda>Y. P w)"
 
 lemma subst_res_def2 [simp]: "(P\<leftarrow>w) Y = P w"
 apply (unfold subst_res_def)
@@ -178,8 +183,9 @@
 
 subsection "subst-Bool"
 
-definition subst_Bool :: "'a assn \<Rightarrow> bool \<Rightarrow> 'a assn" ("_\<leftarrow>=_" [60,61] 60) where
- "P\<leftarrow>=b \<equiv> \<lambda>Y s Z. \<exists>v. P (Val v) s Z \<and> (normal s \<longrightarrow> the_Bool v=b)"
+definition
+  subst_Bool :: "'a assn \<Rightarrow> bool \<Rightarrow> 'a assn" ("_\<leftarrow>=_" [60,61] 60)
+  where "P\<leftarrow>=b = (\<lambda>Y s Z. \<exists>v. P (Val v) s Z \<and> (normal s \<longrightarrow> the_Bool v=b))"
 
 lemma subst_Bool_def2 [simp]: 
 "(P\<leftarrow>=b) Y s Z = (\<exists>v. P (Val v) s Z \<and> (normal s \<longrightarrow> the_Bool v=b))"
@@ -193,8 +199,9 @@
 
 subsection "peek-res"
 
-definition peek_res :: "(res \<Rightarrow> 'a assn) \<Rightarrow> 'a assn" where
- "peek_res Pf \<equiv> \<lambda>Y. Pf Y Y"
+definition
+  peek_res :: "(res \<Rightarrow> 'a assn) \<Rightarrow> 'a assn"
+  where "peek_res Pf = (\<lambda>Y. Pf Y Y)"
 
 syntax
   "_peek_res" :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn"            ("\<lambda>_:. _" [0,3] 3)
@@ -221,8 +228,9 @@
 
 subsection "ign-res"
 
-definition ign_res :: "        'a assn \<Rightarrow> 'a assn" ("_\<down>" [1000] 1000) where
-  "P\<down>        \<equiv> \<lambda>Y s Z. \<exists>Y. P Y s Z"
+definition
+  ign_res :: "'a assn \<Rightarrow> 'a assn" ("_\<down>" [1000] 1000)
+  where "P\<down> = (\<lambda>Y s Z. \<exists>Y. P Y s Z)"
 
 lemma ign_res_def2 [simp]: "P\<down> Y s Z = (\<exists>Y. P Y s Z)"
 apply (unfold ign_res_def)
@@ -252,8 +260,9 @@
 
 subsection "peek-st"
 
-definition peek_st :: "(st \<Rightarrow> 'a assn) \<Rightarrow> 'a assn" where
- "peek_st P \<equiv> \<lambda>Y s. P (store s) Y s"
+definition
+  peek_st :: "(st \<Rightarrow> 'a assn) \<Rightarrow> 'a assn"
+  where "peek_st P = (\<lambda>Y s. P (store s) Y s)"
 
 syntax
   "_peek_st"   :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn"            ("\<lambda>_.. _" [0,3] 3)
@@ -296,8 +305,9 @@
 
 subsection "ign-res-eq"
 
-definition ign_res_eq :: "'a assn \<Rightarrow> res \<Rightarrow> 'a assn" ("_\<down>=_"  [60,61] 60) where
- "P\<down>=w       \<equiv> \<lambda>Y:. P\<down> \<and>. (\<lambda>s. Y=w)"
+definition
+  ign_res_eq :: "'a assn \<Rightarrow> res \<Rightarrow> 'a assn" ("_\<down>=_"  [60,61] 60)
+  where "P\<down>=w \<equiv> (\<lambda>Y:. P\<down> \<and>. (\<lambda>s. Y=w))"
 
 lemma ign_res_eq_def2 [simp]: "(P\<down>=w) Y s Z = ((\<exists>Y. P Y s Z) \<and> Y=w)"
 apply (unfold ign_res_eq_def)
@@ -326,8 +336,9 @@
 
 subsection "RefVar"
 
-definition RefVar :: "(state \<Rightarrow> vvar \<times> state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn" (infixr "..;" 13) where
- "vf ..; P \<equiv> \<lambda>Y s. let (v,s') = vf s in P (Var v) s'"
+definition
+  RefVar :: "(state \<Rightarrow> vvar \<times> state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn" (infixr "..;" 13)
+  where "(vf ..; P) = (\<lambda>Y s. let (v,s') = vf s in P (Var v) s')"
  
 lemma RefVar_def2 [simp]: "(vf ..; P) Y s =  
   P (Var (fst (vf s))) (snd (vf s))"
@@ -337,12 +348,13 @@
 
 subsection "allocation"
 
-definition Alloc :: "prog \<Rightarrow> obj_tag \<Rightarrow> 'a assn \<Rightarrow> 'a assn" where
- "Alloc G otag P \<equiv> \<lambda>Y s Z.
-                   \<forall>s' a. G\<turnstile>s \<midarrow>halloc otag\<succ>a\<rightarrow> s'\<longrightarrow> P (Val (Addr a)) s' Z"
+definition
+  Alloc :: "prog \<Rightarrow> obj_tag \<Rightarrow> 'a assn \<Rightarrow> 'a assn"
+  where "Alloc G otag P = (\<lambda>Y s Z. \<forall>s' a. G\<turnstile>s \<midarrow>halloc otag\<succ>a\<rightarrow> s'\<longrightarrow> P (Val (Addr a)) s' Z)"
 
-definition SXAlloc     :: "prog \<Rightarrow> 'a assn \<Rightarrow> 'a assn" where
- "SXAlloc G P \<equiv> \<lambda>Y s Z. \<forall>s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<longrightarrow> P Y s' Z"
+definition
+  SXAlloc :: "prog \<Rightarrow> 'a assn \<Rightarrow> 'a assn"
+  where "SXAlloc G P = (\<lambda>Y s Z. \<forall>s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<longrightarrow> P Y s' Z)"
 
 
 lemma Alloc_def2 [simp]: "Alloc G otag P Y s Z =  
@@ -359,11 +371,12 @@
 
 section "validity"
 
-definition type_ok :: "prog \<Rightarrow> term \<Rightarrow> state \<Rightarrow> bool" where
- "type_ok G t s \<equiv> 
-    \<exists>L T C A. (normal s \<longrightarrow> \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T \<and> 
-                            \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A )
-              \<and> s\<Colon>\<preceq>(G,L)"
+definition
+  type_ok :: "prog \<Rightarrow> term \<Rightarrow> state \<Rightarrow> bool" where
+  "type_ok G t s =
+    (\<exists>L T C A. (normal s \<longrightarrow> \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T \<and> 
+                             \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A )
+               \<and> s\<Colon>\<preceq>(G,L))"
 
 datatype    'a triple = triple "('a assn)" "term" "('a assn)" (** should be
 something like triple = \<forall>'a. triple ('a assn) term ('a assn)   **)
@@ -407,34 +420,35 @@
 
 definition mtriples :: "('c \<Rightarrow> 'sig \<Rightarrow> 'a assn) \<Rightarrow> ('c \<Rightarrow> 'sig \<Rightarrow> expr) \<Rightarrow> 
                 ('c \<Rightarrow> 'sig \<Rightarrow> 'a assn) \<Rightarrow> ('c \<times>  'sig) set \<Rightarrow> 'a triples" ("{{(1_)}/ _-\<succ>/ {(1_)} | _}"[3,65,3,65]75) where
- "{{P} tf-\<succ> {Q} | ms} \<equiv> (\<lambda>(C,sig). {Normal(P C sig)} tf C sig-\<succ> {Q C sig})`ms"
+ "{{P} tf-\<succ> {Q} | ms} = (\<lambda>(C,sig). {Normal(P C sig)} tf C sig-\<succ> {Q C sig})`ms"
   
-consts
-
- triple_valid :: "prog \<Rightarrow> nat \<Rightarrow>        'a triple  \<Rightarrow> bool"
-                                                (   "_\<Turnstile>_:_" [61,0, 58] 57)
-    ax_valids :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triples \<Rightarrow> bool"
-                                                ("_,_|\<Turnstile>_"   [61,58,58] 57)
+definition
+  triple_valid :: "prog \<Rightarrow> nat \<Rightarrow> 'a triple  \<Rightarrow> bool"  ("_\<Turnstile>_:_" [61,0, 58] 57)
+  where
+    "G\<Turnstile>n:t =
+      (case t of {P} t\<succ> {Q} \<Rightarrow>
+        \<forall>Y s Z. P Y s Z \<longrightarrow> type_ok G t s \<longrightarrow>
+        (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> Q Y' s' Z))"
 
 abbreviation
- triples_valid:: "prog \<Rightarrow> nat \<Rightarrow>         'a triples \<Rightarrow> bool"
-                                                (  "_||=_:_" [61,0, 58] 57)
- where "G||=n:ts == Ball ts (triple_valid G n)"
+  triples_valid:: "prog \<Rightarrow> nat \<Rightarrow> 'a triples \<Rightarrow> bool"  (  "_||=_:_" [61,0, 58] 57)
+  where "G||=n:ts == Ball ts (triple_valid G n)"
+
+notation (xsymbols)
+  triples_valid  ("_|\<Turnstile>_:_" [61,0, 58] 57)
+
+
+definition
+  ax_valids :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triples \<Rightarrow> bool"  ("_,_|\<Turnstile>_" [61,58,58] 57)
+  where "(G,A|\<Turnstile>ts) = (\<forall>n. G|\<Turnstile>n:A \<longrightarrow> G|\<Turnstile>n:ts)"
 
 abbreviation
- ax_valid :: "prog \<Rightarrow>  'b triples \<Rightarrow> 'a triple  \<Rightarrow> bool"
-                                                ( "_,_|=_"   [61,58,58] 57)
- where "G,A |=t == G,A|\<Turnstile>{t}"
+  ax_valid :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triple \<Rightarrow> bool"  ( "_,_|=_"   [61,58,58] 57)
+  where "G,A |=t == G,A|\<Turnstile>{t}"
 
 notation (xsymbols)
-  triples_valid  ("_|\<Turnstile>_:_" [61,0, 58] 57) and
   ax_valid  ("_,_\<Turnstile>_" [61,58,58] 57)
 
-defs  triple_valid_def:  "G\<Turnstile>n:t  \<equiv> case t of {P} t\<succ> {Q} \<Rightarrow>
-                          \<forall>Y s Z. P Y s Z \<longrightarrow> type_ok G t s \<longrightarrow>
-                          (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> Q Y' s' Z)"
-
-defs  ax_valids_def:"G,A|\<Turnstile>ts  \<equiv>  \<forall>n. G|\<Turnstile>n:A \<longrightarrow> G|\<Turnstile>n:ts"
 
 lemma triple_valid_def2: "G\<Turnstile>n:{P} t\<succ> {Q} =  
  (\<forall>Y s Z. P Y s Z 
@@ -625,8 +639,9 @@
 axioms 
 *)
 
-definition adapt_pre :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn" where
-"adapt_pre P Q Q'\<equiv>\<lambda>Y s Z. \<forall>Y' s'. \<exists>Z'. P Y s Z' \<and> (Q Y' s' Z' \<longrightarrow> Q' Y' s' Z)"
+definition
+  adapt_pre :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn"
+  where "adapt_pre P Q Q' = (\<lambda>Y s Z. \<forall>Y' s'. \<exists>Z'. P Y s Z' \<and> (Q Y' s' Z' \<longrightarrow> Q' Y' s' Z))"
 
 
 section "rules derived by induction"
diff -r d9549f9da779 -r a79abb22ca9c src/HOL/Bali/AxSound.thy
--- a/src/HOL/Bali/AxSound.thy	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/AxSound.thy	Mon Jul 26 18:25:19 2010 +0200
@@ -9,18 +9,15 @@
 
 section "validity"
 
-consts
-
- triple_valid2:: "prog \<Rightarrow> nat \<Rightarrow>        'a triple  \<Rightarrow> bool"
-                                                (   "_\<Turnstile>_\<Colon>_"[61,0, 58] 57)
-    ax_valids2:: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool"
-                                                ("_,_|\<Turnstile>\<Colon>_" [61,58,58] 57)
-
-defs  triple_valid2_def: "G\<Turnstile>n\<Colon>t \<equiv> case t of {P} t\<succ> {Q} \<Rightarrow>
- \<forall>Y s Z. P Y s Z \<longrightarrow> (\<forall>L. s\<Colon>\<preceq>(G,L) 
- \<longrightarrow> (\<forall>T C A. (normal s \<longrightarrow> (\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T \<and> 
-                            \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A)) \<longrightarrow>
- (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> Q Y' s' Z \<and> s'\<Colon>\<preceq>(G,L))))"
+definition
+  triple_valid2 :: "prog \<Rightarrow> nat \<Rightarrow> 'a triple \<Rightarrow> bool"  ("_\<Turnstile>_\<Colon>_"[61,0, 58] 57)
+  where
+    "G\<Turnstile>n\<Colon>t =
+      (case t of {P} t\<succ> {Q} \<Rightarrow>
+        \<forall>Y s Z. P Y s Z \<longrightarrow> (\<forall>L. s\<Colon>\<preceq>(G,L)
+          \<longrightarrow> (\<forall>T C A. (normal s \<longrightarrow> (\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T \<and>
+            \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A)) \<longrightarrow>
+             (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> Q Y' s' Z \<and> s'\<Colon>\<preceq>(G,L)))))"
 
 text {* This definition differs from the ordinary  @{text triple_valid_def} 
 manly in the conclusion: We also ensures conformance of the result state. So
@@ -29,8 +26,10 @@
 proof of the axiomatic semantics, in the end we will conclude to 
 the ordinary definition.
 *}
- 
-defs  ax_valids2_def:    "G,A|\<Turnstile>\<Colon>ts \<equiv>  \<forall>n. (\<forall>t\<in>A. G\<Turnstile>n\<Colon>t) \<longrightarrow> (\<forall>t\<in>ts. G\<Turnstile>n\<Colon>t)"
+
+definition
+  ax_valids2 :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool"  ("_,_|\<Turnstile>\<Colon>_" [61,58,58] 57)
+  where "G,A|\<Turnstile>\<Colon>ts = (\<forall>n. (\<forall>t\<in>A. G\<Turnstile>n\<Colon>t) \<longrightarrow> (\<forall>t\<in>ts. G\<Turnstile>n\<Colon>t))"
 
 lemma triple_valid2_def2: "G\<Turnstile>n\<Colon>{P} t\<succ> {Q} =  
  (\<forall>Y s Z. P Y s Z \<longrightarrow> (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s')\<longrightarrow>  
diff -r d9549f9da779 -r a79abb22ca9c src/HOL/Bali/Basis.thy
--- a/src/HOL/Bali/Basis.thy	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/Basis.thy	Mon Jul 26 18:25:19 2010 +0200
@@ -180,31 +180,34 @@
 
 notation sum_case  (infixr "'(+')"80)
 
-consts    the_Inl  :: "'a + 'b \<Rightarrow> 'a"
-          the_Inr  :: "'a + 'b \<Rightarrow> 'b"
-primrec  "the_Inl (Inl a) = a"
-primrec  "the_Inr (Inr b) = b"
+primrec the_Inl  :: "'a + 'b \<Rightarrow> 'a"
+  where "the_Inl (Inl a) = a"
+
+primrec the_Inr  :: "'a + 'b \<Rightarrow> 'b"
+  where "the_Inr (Inr b) = b"
 
 datatype ('a, 'b, 'c) sum3 = In1 'a | In2 'b | In3 'c
 
-consts    the_In1  :: "('a, 'b, 'c) sum3 \<Rightarrow> 'a"
-          the_In2  :: "('a, 'b, 'c) sum3 \<Rightarrow> 'b"
-          the_In3  :: "('a, 'b, 'c) sum3 \<Rightarrow> 'c"
-primrec  "the_In1 (In1 a) = a"
-primrec  "the_In2 (In2 b) = b"
-primrec  "the_In3 (In3 c) = c"
+primrec the_In1  :: "('a, 'b, 'c) sum3 \<Rightarrow> 'a"
+  where "the_In1 (In1 a) = a"
+
+primrec the_In2  :: "('a, 'b, 'c) sum3 \<Rightarrow> 'b"
+  where "the_In2 (In2 b) = b"
+
+primrec the_In3  :: "('a, 'b, 'c) sum3 \<Rightarrow> 'c"
+  where "the_In3 (In3 c) = c"
 
 abbreviation In1l   :: "'al \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
-      where "In1l e == In1 (Inl e)"
+  where "In1l e == In1 (Inl e)"
 
 abbreviation In1r   :: "'ar \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
-      where "In1r c == In1 (Inr c)"
+  where "In1r c == In1 (Inr c)"
 
 abbreviation the_In1l :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'al"
-      where "the_In1l == the_Inl \<circ> the_In1"
+  where "the_In1l == the_Inl \<circ> the_In1"
 
 abbreviation the_In1r :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'ar"
-      where "the_In1r == the_Inr \<circ> the_In1"
+  where "the_In1r == the_Inr \<circ> the_In1"
 
 ML {*
 fun sum3_instantiate ctxt thm = map (fn s =>
@@ -232,8 +235,9 @@
 
 text{* Deemed too special for theory Map. *}
 
-definition chg_map :: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)" where
- "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
+definition
+  chg_map :: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)"
+  where "chg_map f a m = (case m a of None => m | Some b => m(a|->f b))"
 
 lemma chg_map_new[simp]: "m a = None   ==> chg_map f a m = m"
 by (unfold chg_map_def, auto)
@@ -247,8 +251,9 @@
 
 section "unique association lists"
 
-definition unique :: "('a \<times> 'b) list \<Rightarrow> bool" where
- "unique \<equiv> distinct \<circ> map fst"
+definition
+  unique :: "('a \<times> 'b) list \<Rightarrow> bool"
+  where "unique = distinct \<circ> map fst"
 
 lemma uniqueD [rule_format (no_asm)]: 
 "unique l--> (!x y. (x,y):set l --> (!x' y'. (x',y'):set l --> x=x'-->  y=y'))"
@@ -296,11 +301,11 @@
 
 section "list patterns"
 
-consts
-  lsplit         :: "[['a, 'a list] => 'b, 'a list] => 'b"
-defs
-  lsplit_def:    "lsplit == %f l. f (hd l) (tl l)"
-(*  list patterns -- extends pre-defined type "pttrn" used in abstractions *)
+definition
+  lsplit :: "[['a, 'a list] => 'b, 'a list] => 'b" where
+  "lsplit = (\<lambda>f l. f (hd l) (tl l))"
+
+text {* list patterns -- extends pre-defined type "pttrn" used in abstractions *}
 syntax
   "_lpttrn"    :: "[pttrn,pttrn] => pttrn"     ("_#/_" [901,900] 900)
 translations
diff -r d9549f9da779 -r a79abb22ca9c src/HOL/Bali/Conform.thy
--- a/src/HOL/Bali/Conform.thy	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/Conform.thy	Mon Jul 26 18:25:19 2010 +0200
@@ -96,8 +96,8 @@
 
 section "value conformance"
 
-definition conf :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>_"   [71,71,71,71] 70) where
-           "G,s\<turnstile>v\<Colon>\<preceq>T \<equiv> \<exists>T'\<in>typeof (\<lambda>a. Option.map obj_ty (heap s a)) v:G\<turnstile>T'\<preceq>T"
+definition conf :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>_"   [71,71,71,71] 70)
+  where "G,s\<turnstile>v\<Colon>\<preceq>T = (\<exists>T'\<in>typeof (\<lambda>a. Option.map obj_ty (heap s a)) v:G\<turnstile>T'\<preceq>T)"
 
 lemma conf_cong [simp]: "G,set_locals l s\<turnstile>v\<Colon>\<preceq>T = G,s\<turnstile>v\<Colon>\<preceq>T"
 by (auto simp: conf_def)
@@ -177,8 +177,9 @@
 
 section "value list conformance"
 
-definition lconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool" ("_,_\<turnstile>_[\<Colon>\<preceq>]_" [71,71,71,71] 70) where
-           "G,s\<turnstile>vs[\<Colon>\<preceq>]Ts \<equiv> \<forall>n. \<forall>T\<in>Ts n: \<exists>v\<in>vs n: G,s\<turnstile>v\<Colon>\<preceq>T"
+definition
+  lconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool" ("_,_\<turnstile>_[\<Colon>\<preceq>]_" [71,71,71,71] 70)
+  where "G,s\<turnstile>vs[\<Colon>\<preceq>]Ts = (\<forall>n. \<forall>T\<in>Ts n: \<exists>v\<in>vs n: G,s\<turnstile>v\<Colon>\<preceq>T)"
 
 lemma lconfD: "\<lbrakk>G,s\<turnstile>vs[\<Colon>\<preceq>]Ts; Ts n = Some T\<rbrakk> \<Longrightarrow> G,s\<turnstile>(the (vs n))\<Colon>\<preceq>T"
 by (force simp: lconf_def)
@@ -260,8 +261,9 @@
 *}
 
   
-definition wlconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool" ("_,_\<turnstile>_[\<sim>\<Colon>\<preceq>]_" [71,71,71,71] 70) where
-           "G,s\<turnstile>vs[\<sim>\<Colon>\<preceq>]Ts \<equiv> \<forall>n. \<forall>T\<in>Ts n: \<forall> v\<in>vs n: G,s\<turnstile>v\<Colon>\<preceq>T"
+definition
+  wlconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool" ("_,_\<turnstile>_[\<sim>\<Colon>\<preceq>]_" [71,71,71,71] 70)
+  where "G,s\<turnstile>vs[\<sim>\<Colon>\<preceq>]Ts = (\<forall>n. \<forall>T\<in>Ts n: \<forall> v\<in>vs n: G,s\<turnstile>v\<Colon>\<preceq>T)"
 
 lemma wlconfD: "\<lbrakk>G,s\<turnstile>vs[\<sim>\<Colon>\<preceq>]Ts; Ts n = Some T; vs n = Some v\<rbrakk> \<Longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>T"
 by (auto simp: wlconf_def)
@@ -338,11 +340,12 @@
 
 section "object conformance"
 
-definition oconf :: "prog \<Rightarrow> st \<Rightarrow> obj \<Rightarrow> oref \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>\<surd>_"  [71,71,71,71] 70) where
-           "G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r \<equiv> G,s\<turnstile>values obj[\<Colon>\<preceq>]var_tys G (tag obj) r \<and> 
+definition
+  oconf :: "prog \<Rightarrow> st \<Rightarrow> obj \<Rightarrow> oref \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>\<surd>_"  [71,71,71,71] 70) where
+  "(G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r) = (G,s\<turnstile>values obj[\<Colon>\<preceq>]var_tys G (tag obj) r \<and> 
                            (case r of 
                               Heap a \<Rightarrow> is_type G (obj_ty obj) 
-                            | Stat C \<Rightarrow> True)"
+                            | Stat C \<Rightarrow> True))"
 
 
 lemma oconf_is_type: "G,s\<turnstile>obj\<Colon>\<preceq>\<surd>Heap a \<Longrightarrow> is_type G (obj_ty obj)"
@@ -373,12 +376,14 @@
 
 section "state conformance"
 
-definition conforms :: "state \<Rightarrow> env' \<Rightarrow> bool"   ("_\<Colon>\<preceq>_"   [71,71]      70)  where
-   "xs\<Colon>\<preceq>E \<equiv> 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>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)"
+definition
+  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>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))"
 
 section "conforms"
 
diff -r d9549f9da779 -r a79abb22ca9c src/HOL/Bali/Decl.thy
--- a/src/HOL/Bali/Decl.thy	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/Decl.thy	Mon Jul 26 18:25:19 2010 +0200
@@ -206,8 +206,9 @@
   (type) "mdecl" <= (type) "sig \<times> methd"
 
 
-definition mhead :: "methd \<Rightarrow> mhead" where
-  "mhead m \<equiv> \<lparr>access=access m, static=static m, pars=pars m, resT=resT m\<rparr>"
+definition
+  mhead :: "methd \<Rightarrow> mhead"
+  where "mhead m = \<lparr>access=access m, static=static m, pars=pars m, resT=resT m\<rparr>"
 
 lemma access_mhead [simp]:"access (mhead m) = access m"
 by (simp add: mhead_def)
@@ -237,7 +238,7 @@
 
 definition
 memberdecl_memberid_def:
-  "memberid m \<equiv> (case m of
+  "memberid m = (case m of
                     fdecl (vn,f)  \<Rightarrow> fid vn
                   | mdecl (sig,m) \<Rightarrow> mid sig)"
 
@@ -262,7 +263,7 @@
 
 definition
 pair_memberid_def:
-  "memberid p \<equiv> memberid (snd p)"
+  "memberid p = memberid (snd p)"
 
 instance ..
 
@@ -274,8 +275,9 @@
 lemma memberid_pair_simp1: "memberid p  = memberid (snd p)"
 by (simp add: pair_memberid_def)
 
-definition is_field :: "qtname \<times> memberdecl \<Rightarrow> bool" where
-"is_field m \<equiv> \<exists> declC f. m=(declC,fdecl f)"
+definition
+  is_field :: "qtname \<times> memberdecl \<Rightarrow> bool"
+  where "is_field m = (\<exists> declC f. m=(declC,fdecl f))"
   
 lemma is_fieldD: "is_field m \<Longrightarrow> \<exists> declC f. m=(declC,fdecl f)"
 by (simp add: is_field_def)
@@ -283,8 +285,9 @@
 lemma is_fieldI: "is_field (C,fdecl f)"
 by (simp add: is_field_def)
 
-definition is_method :: "qtname \<times> memberdecl \<Rightarrow> bool" where
-"is_method membr \<equiv> \<exists> declC m. membr=(declC,mdecl m)"
+definition
+  is_method :: "qtname \<times> memberdecl \<Rightarrow> bool"
+  where "is_method membr = (\<exists>declC m. membr=(declC,mdecl m))"
   
 lemma is_methodD: "is_method membr \<Longrightarrow> \<exists> declC m. membr=(declC,mdecl m)"
 by (simp add: is_method_def)
@@ -314,8 +317,9 @@
                       isuperIfs::qtname list,\<dots>::'a\<rparr>"
   (type) "idecl" <= (type) "qtname \<times> iface"
 
-definition ibody :: "iface \<Rightarrow> ibody" where
-  "ibody i \<equiv> \<lparr>access=access i,imethods=imethods i\<rparr>"
+definition
+  ibody :: "iface \<Rightarrow> ibody"
+  where "ibody i = \<lparr>access=access i,imethods=imethods i\<rparr>"
 
 lemma access_ibody [simp]: "(access (ibody i)) = access i"
 by (simp add: ibody_def)
@@ -349,8 +353,9 @@
                       super::qtname,superIfs::qtname list,\<dots>::'a\<rparr>"
   (type) "cdecl" <= (type) "qtname \<times> class"
 
-definition cbody :: "class \<Rightarrow> cbody" where
-  "cbody c \<equiv> \<lparr>access=access c, cfields=cfields c,methods=methods c,init=init c\<rparr>"
+definition
+  cbody :: "class \<Rightarrow> cbody"
+  where "cbody c = \<lparr>access=access c, cfields=cfields c,methods=methods c,init=init c\<rparr>"
 
 lemma access_cbody [simp]:"access (cbody c) = access c"
 by (simp add: cbody_def)
@@ -368,18 +373,17 @@
 section "standard classes"
 
 consts
-
   Object_mdecls  ::  "mdecl list" --{* methods of Object *}
   SXcpt_mdecls   ::  "mdecl list" --{* methods of SXcpts *}
-  ObjectC ::         "cdecl"      --{* declaration  of root      class   *}
-  SXcptC  ::"xname \<Rightarrow> cdecl"      --{* declarations of throwable classes *}
-
-defs 
 
+definition
+  ObjectC ::         "cdecl"      --{* declaration  of root      class   *} where
+  "ObjectC = (Object,\<lparr>access=Public,cfields=[],methods=Object_mdecls,
+                                  init=Skip,super=undefined,superIfs=[]\<rparr>)"
 
-ObjectC_def:"ObjectC  \<equiv> (Object,\<lparr>access=Public,cfields=[],methods=Object_mdecls,
-                                  init=Skip,super=undefined,superIfs=[]\<rparr>)"
-SXcptC_def:"SXcptC xn\<equiv> (SXcpt xn,\<lparr>access=Public,cfields=[],methods=SXcpt_mdecls,
+definition
+  SXcptC  ::"xname \<Rightarrow> cdecl"      --{* declarations of throwable classes *} where
+  "SXcptC xn = (SXcpt xn,\<lparr>access=Public,cfields=[],methods=SXcpt_mdecls,
                                    init=Skip,
                                    super=if xn = Throwable then Object 
                                                            else SXcpt Throwable,
@@ -391,8 +395,9 @@
 lemma SXcptC_inject [simp]: "(SXcptC xn = SXcptC xm) = (xn = xm)"
 by (simp add: SXcptC_def)
 
-definition standard_classes :: "cdecl list" where
-         "standard_classes \<equiv> [ObjectC, SXcptC Throwable,
+definition
+  standard_classes :: "cdecl list" where
+  "standard_classes = [ObjectC, SXcptC Throwable,
                 SXcptC NullPointer, SXcptC OutOfMemory, SXcptC ClassCast,
                 SXcptC NegArrSize , SXcptC IndOutBound, SXcptC ArrStore]"
 
@@ -426,16 +431,15 @@
 
 section "is type"
 
-consts
-  is_type :: "prog \<Rightarrow>     ty \<Rightarrow> bool"
-  isrtype :: "prog \<Rightarrow> ref_ty \<Rightarrow> bool"
-
-primrec "is_type G (PrimT pt)  = True"
-        "is_type G (RefT  rt)  = isrtype G rt"
-        "isrtype G (NullT    ) = True"
-        "isrtype G (IfaceT tn) = is_iface G tn"
-        "isrtype G (ClassT tn) = is_class G tn"
-        "isrtype G (ArrayT T ) = is_type  G T"
+primrec is_type :: "prog \<Rightarrow> ty \<Rightarrow> bool"
+  and isrtype :: "prog \<Rightarrow> ref_ty \<Rightarrow> bool"
+where
+  "is_type G (PrimT pt)  = True"
+| "is_type G (RefT  rt)  = isrtype G rt"
+| "isrtype G (NullT) = True"
+| "isrtype G (IfaceT tn) = is_iface G tn"
+| "isrtype G (ClassT tn) = is_class G tn"
+| "isrtype G (ArrayT T ) = is_type  G T"
 
 lemma type_is_iface: "is_type G (Iface I) \<Longrightarrow> is_iface G I"
 by auto
@@ -446,13 +450,13 @@
 
 section "subinterface and subclass relation, in anticipation of TypeRel.thy"
 
-consts 
+definition
   subint1  :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct subinterface *}
-  subcls1  :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct subclass     *}
+  where "subint1 G = {(I,J). \<exists>i\<in>iface G I: J\<in>set (isuperIfs i)}"
 
-defs
-  subint1_def: "subint1 G \<equiv> {(I,J). \<exists>i\<in>iface G I: J\<in>set (isuperIfs i)}"
-  subcls1_def: "subcls1 G \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c\<in>class G C: super c = D)}"
+definition
+  subcls1  :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct subclass *}
+  where "subcls1 G = {(C,D). C\<noteq>Object \<and> (\<exists>c\<in>class G C: super c = D)}"
 
 abbreviation
   subcls1_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70)
@@ -517,15 +521,18 @@
 
 section "well-structured programs"
 
-definition ws_idecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname list \<Rightarrow> bool" where
- "ws_idecl G I si \<equiv> \<forall>J\<in>set si.  is_iface G J   \<and> (J,I)\<notin>(subint1 G)^+"
+definition
+  ws_idecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname list \<Rightarrow> bool"
+  where "ws_idecl G I si = (\<forall>J\<in>set si.  is_iface G J   \<and> (J,I)\<notin>(subint1 G)^+)"
   
-definition ws_cdecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" where
- "ws_cdecl G C sc \<equiv> C\<noteq>Object \<longrightarrow> is_class G sc \<and> (sc,C)\<notin>(subcls1 G)^+"
+definition
+  ws_cdecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
+  where "ws_cdecl G C sc = (C\<noteq>Object \<longrightarrow> is_class G sc \<and> (sc,C)\<notin>(subcls1 G)^+)"
   
-definition ws_prog  :: "prog \<Rightarrow> bool" where
- "ws_prog G \<equiv> (\<forall>(I,i)\<in>set (ifaces  G). ws_idecl G I (isuperIfs i)) \<and> 
-              (\<forall>(C,c)\<in>set (classes G). ws_cdecl G C (super c))"
+definition
+  ws_prog  :: "prog \<Rightarrow> bool" where
+  "ws_prog G = ((\<forall>(I,i)\<in>set (ifaces  G). ws_idecl G I (isuperIfs i)) \<and> 
+                 (\<forall>(C,c)\<in>set (classes G). ws_cdecl G C (super c)))"
 
 
 lemma ws_progI: 
@@ -810,10 +817,10 @@
 apply simp
 done
 
-definition imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
+definition
+  imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
   --{* methods of an interface, with overriding and inheritance, cf. 9.2 *}
-"imethds G I 
-  \<equiv> iface_rec G I  
+  "imethds G I = iface_rec G I
               (\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus> 
                         (Option.set \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
         
diff -r d9549f9da779 -r a79abb22ca9c src/HOL/Bali/DeclConcepts.thy
--- a/src/HOL/Bali/DeclConcepts.thy	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/DeclConcepts.thy	Mon Jul 26 18:25:19 2010 +0200
@@ -9,7 +9,7 @@
 section "access control (cf. 6.6), overriding and hiding (cf. 8.4.6.1)"
 
 definition is_public :: "prog \<Rightarrow> qtname \<Rightarrow> bool" where
-"is_public G qn \<equiv> (case class G qn of
+"is_public G qn = (case class G qn of
                      None       \<Rightarrow> (case iface G qn of
                                       None       \<Rightarrow> False
                                     | Some i \<Rightarrow> access i = Public)
@@ -21,33 +21,35 @@
 in their package or if they are defined public, an array type is accessible if
 its element type is accessible *}
  
-consts accessible_in   :: "prog \<Rightarrow> ty     \<Rightarrow> pname \<Rightarrow> bool"  
-                                      ("_ \<turnstile> _ accessible'_in _" [61,61,61] 60)
-       rt_accessible_in:: "prog \<Rightarrow> ref_ty \<Rightarrow> pname \<Rightarrow> bool" 
-                                      ("_ \<turnstile> _ accessible'_in' _" [61,61,61] 60) 
 primrec
-"G\<turnstile>(PrimT p)   accessible_in pack  = True"
-accessible_in_RefT_simp: 
-"G\<turnstile>(RefT  r)   accessible_in pack  = G\<turnstile>r accessible_in' pack"
-
-"G\<turnstile>(NullT)     accessible_in' pack = True"
-"G\<turnstile>(IfaceT I)  accessible_in' pack = ((pid I = pack) \<or> is_public G I)"
-"G\<turnstile>(ClassT C)  accessible_in' pack = ((pid C = pack) \<or> is_public G C)"
-"G\<turnstile>(ArrayT ty) accessible_in' pack = G\<turnstile>ty accessible_in pack"
+  accessible_in :: "prog \<Rightarrow> ty \<Rightarrow> pname \<Rightarrow> bool"  ("_ \<turnstile> _ accessible'_in _" [61,61,61] 60) and
+  rt_accessible_in :: "prog \<Rightarrow> ref_ty \<Rightarrow> pname \<Rightarrow> bool"  ("_ \<turnstile> _ accessible'_in' _" [61,61,61] 60)
+where
+  "G\<turnstile>(PrimT p) accessible_in pack = True"
+| accessible_in_RefT_simp:
+  "G\<turnstile>(RefT  r) accessible_in pack = G\<turnstile>r accessible_in' pack"
+| "G\<turnstile>(NullT) accessible_in' pack = True"
+| "G\<turnstile>(IfaceT I) accessible_in' pack = ((pid I = pack) \<or> is_public G I)"
+| "G\<turnstile>(ClassT C) accessible_in' pack = ((pid C = pack) \<or> is_public G C)"
+| "G\<turnstile>(ArrayT ty) accessible_in' pack = G\<turnstile>ty accessible_in pack"
 
 declare accessible_in_RefT_simp [simp del]
 
-definition is_acc_class :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool" where
-    "is_acc_class G P C \<equiv> is_class G C \<and> G\<turnstile>(Class C) accessible_in P"
+definition
+  is_acc_class :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool"
+  where "is_acc_class G P C = (is_class G C \<and> G\<turnstile>(Class C) accessible_in P)"
 
-definition is_acc_iface :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool" where
-    "is_acc_iface G P I \<equiv> is_iface G I \<and> G\<turnstile>(Iface I) accessible_in P"
+definition
+  is_acc_iface :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool"
+  where "is_acc_iface G P I = (is_iface G I \<and> G\<turnstile>(Iface I) accessible_in P)"
 
-definition is_acc_type  :: "prog \<Rightarrow> pname \<Rightarrow> ty     \<Rightarrow> bool" where
-    "is_acc_type  G P T \<equiv> is_type G T  \<and> G\<turnstile>T accessible_in P"
+definition
+  is_acc_type :: "prog \<Rightarrow> pname \<Rightarrow> ty \<Rightarrow> bool"
+  where "is_acc_type  G P T = (is_type G T  \<and> G\<turnstile>T accessible_in P)"
 
-definition is_acc_reftype  :: "prog \<Rightarrow> pname \<Rightarrow> ref_ty \<Rightarrow> bool" where
-  "is_acc_reftype  G P T \<equiv> isrtype G T  \<and> G\<turnstile>T accessible_in' P"
+definition
+  is_acc_reftype  :: "prog \<Rightarrow> pname \<Rightarrow> ref_ty \<Rightarrow> bool"
+  where "is_acc_reftype G P T = (isrtype G T  \<and> G\<turnstile>T accessible_in' P)"
 
 lemma is_acc_classD:
  "is_acc_class G P C \<Longrightarrow>  is_class G C \<and> G\<turnstile>(Class C) accessible_in P"
@@ -87,7 +89,7 @@
 begin
 
 definition
-  acc_modi_accmodi_def: "accmodi (a::acc_modi) \<equiv> a"
+  acc_modi_accmodi_def: "accmodi (a::acc_modi) = a"
 
 instance ..
 
@@ -100,7 +102,7 @@
 begin
 
 definition
-  decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) \<equiv> access d"
+  decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) = access d"
 
 instance ..
 
@@ -113,7 +115,7 @@
 begin
 
 definition
-  pair_acc_modi_def: "accmodi p \<equiv> (accmodi (snd p))"
+  pair_acc_modi_def: "accmodi p = accmodi (snd p)"
 
 instance ..
 
@@ -126,7 +128,7 @@
 begin
 
 definition
-  memberdecl_acc_modi_def: "accmodi m \<equiv> (case m of
+  memberdecl_acc_modi_def: "accmodi m = (case m of
                                           fdecl f \<Rightarrow> accmodi f
                                         | mdecl m \<Rightarrow> accmodi m)"
 
@@ -152,7 +154,7 @@
 begin
 
 definition
-  "declclass q \<equiv> \<lparr> pid = pid q, tid = tid q \<rparr>"
+  "declclass q = \<lparr> pid = pid q, tid = tid q \<rparr>"
 
 instance ..
 
@@ -169,7 +171,7 @@
 begin
 
 definition
-  pair_declclass_def: "declclass p \<equiv> declclass (fst p)"
+  pair_declclass_def: "declclass p = declclass (fst p)"
 
 instance ..
 
@@ -208,7 +210,7 @@
 begin
 
 definition
-  pair_is_static_def: "is_static p \<equiv> is_static (snd p)"
+  pair_is_static_def: "is_static p = is_static (snd p)"
 
 instance ..
 
@@ -225,7 +227,7 @@
 
 definition
 memberdecl_is_static_def: 
- "is_static m \<equiv> (case m of
+ "is_static m = (case m of
                     fdecl f \<Rightarrow> is_static f
                   | mdecl m \<Rightarrow> is_static m)"
 
@@ -246,28 +248,34 @@
 
 -- {* some mnemotic selectors for various pairs *} 
 
-definition decliface :: "qtname \<times> 'a decl_scheme \<Rightarrow> qtname" where
+definition
+  decliface :: "qtname \<times> 'a decl_scheme \<Rightarrow> qtname" where
   "decliface = fst"          --{* get the interface component *}
 
-definition mbr :: "qtname \<times> memberdecl \<Rightarrow> memberdecl" where
+definition
+  mbr :: "qtname \<times> memberdecl \<Rightarrow> memberdecl" where
   "mbr = snd"            --{* get the memberdecl component *}
 
-definition mthd :: "'b \<times> 'a \<Rightarrow> 'a" where
+definition
+  mthd :: "'b \<times> 'a \<Rightarrow> 'a" where
   "mthd = snd"              --{* get the method component *}
     --{* also used for mdecl, mhead *}
 
-definition fld :: "'b \<times> 'a decl_scheme \<Rightarrow> 'a decl_scheme" where
+definition
+  fld :: "'b \<times> 'a decl_scheme \<Rightarrow> 'a decl_scheme" where
   "fld = snd"               --{* get the field component *}
     --{* also used for @{text "((vname \<times> qtname)\<times> field)"} *}
 
 -- {* some mnemotic selectors for @{text "(vname \<times> qtname)"} *}
 
-definition fname:: "vname \<times> 'a \<Rightarrow> vname" where 
-  "fname = fst"
+definition
+  fname:: "vname \<times> 'a \<Rightarrow> vname"
+  where "fname = fst"
     --{* also used for fdecl *}
 
-definition declclassf:: "(vname \<times> qtname) \<Rightarrow> qtname" where
-  "declclassf = snd"
+definition
+  declclassf:: "(vname \<times> qtname) \<Rightarrow> qtname"
+  where "declclassf = snd"
 
 
 lemma decliface_simp[simp]: "decliface (I,m) = I"
@@ -320,11 +328,13 @@
 
   --{* some mnemotic selectors for @{text "(vname \<times> qtname)"} *}
 
-definition fldname :: "vname \<times> qtname \<Rightarrow> vname"  where
-  "fldname = fst"
+definition
+  fldname :: "vname \<times> qtname \<Rightarrow> vname"
+  where "fldname = fst"
 
-definition fldclass :: "vname \<times> qtname \<Rightarrow> qtname" where
-  "fldclass = snd"
+definition
+  fldclass :: "vname \<times> qtname \<Rightarrow> qtname"
+  where "fldclass = snd"
 
 lemma fldname_simp[simp]: "fldname (n,c) = n"
 by (simp add: fldname_def)
@@ -338,8 +348,9 @@
 text {* Convert a qualified method declaration (qualified with its declaring 
 class) to a qualified member declaration:  @{text methdMembr}  *}
 
-definition methdMembr :: "qtname \<times> mdecl \<Rightarrow> qtname \<times> memberdecl" where
- "methdMembr m = (fst m, mdecl (snd m))"
+definition
+  methdMembr :: "qtname \<times> mdecl \<Rightarrow> qtname \<times> memberdecl"
+  where "methdMembr m = (fst m, mdecl (snd m))"
 
 lemma methdMembr_simp[simp]: "methdMembr (c,m) = (c,mdecl m)"
 by (simp add: methdMembr_def)
@@ -356,8 +367,9 @@
 text {* Convert a qualified method (qualified with its declaring 
 class) to a qualified member declaration:  @{text method}  *}
 
-definition method :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)" where 
-"method sig m \<equiv> (declclass m, mdecl (sig, mthd m))"
+definition
+  method :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)"
+  where "method sig m = (declclass m, mdecl (sig, mthd m))"
 
 lemma method_simp[simp]: "method sig (C,m) = (C,mdecl (sig,m))"
 by (simp add: method_def)
@@ -377,8 +389,9 @@
 lemma memberid_method_simp[simp]:  "memberid (method sig m) = mid sig"
   by (simp add: method_def) 
 
-definition fieldm :: "vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> (qtname \<times> memberdecl)" where 
-"fieldm n f \<equiv> (declclass f, fdecl (n, fld f))"
+definition
+  fieldm :: "vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> (qtname \<times> memberdecl)"
+  where "fieldm n f = (declclass f, fdecl (n, fld f))"
 
 lemma fieldm_simp[simp]: "fieldm n (C,f) = (C,fdecl (n,f))"
 by (simp add: fieldm_def)
@@ -401,8 +414,9 @@
 text {* Select the signature out of a qualified method declaration:
  @{text msig} *}
 
-definition msig :: "(qtname \<times> mdecl) \<Rightarrow> sig" where
-"msig m \<equiv> fst (snd m)"
+definition
+  msig :: "(qtname \<times> mdecl) \<Rightarrow> sig"
+  where "msig m = fst (snd m)"
 
 lemma msig_simp[simp]: "msig (c,(s,m)) = s"
 by (simp add: msig_def)
@@ -410,8 +424,9 @@
 text {* Convert a qualified method (qualified with its declaring 
 class) to a qualified method declaration:  @{text qmdecl}  *}
 
-definition qmdecl :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> mdecl)" where
-"qmdecl sig m \<equiv> (declclass m, (sig,mthd m))"
+definition
+  qmdecl :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> mdecl)"
+  where "qmdecl sig m = (declclass m, (sig,mthd m))"
 
 lemma qmdecl_simp[simp]: "qmdecl sig (C,m) = (C,(sig,m))"
 by (simp add: qmdecl_def)
@@ -476,7 +491,7 @@
 begin
 
 definition
-  pair_resTy_def: "resTy p \<equiv> resTy (snd p)"
+  pair_resTy_def: "resTy p = resTy (snd p)"
 
 instance ..
 
@@ -503,14 +518,15 @@
       it is not accessible for inheritance at all.
 \end{itemize}
 *}
-definition inheritable_in :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> pname \<Rightarrow> bool" ("_ \<turnstile> _ inheritable'_in _" [61,61,61] 60) where
-                  
-"G\<turnstile>membr inheritable_in pack 
-  \<equiv> (case (accmodi membr) of
-       Private   \<Rightarrow> False
-     | Package   \<Rightarrow> (pid (declclass membr)) = pack
-     | Protected \<Rightarrow> True
-     | Public    \<Rightarrow> True)"
+definition
+  inheritable_in :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> pname \<Rightarrow> bool" ("_ \<turnstile> _ inheritable'_in _" [61,61,61] 60)
+where
+"G\<turnstile>membr inheritable_in pack =
+  (case (accmodi membr) of
+     Private   \<Rightarrow> False
+   | Package   \<Rightarrow> (pid (declclass membr)) = pack
+   | Protected \<Rightarrow> True
+   | Public    \<Rightarrow> True)"
 
 abbreviation
 Method_inheritable_in_syntax::
@@ -526,24 +542,26 @@
 
 subsubsection "declared-in/undeclared-in"
 
-definition cdeclaredmethd :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,methd) table" where
-"cdeclaredmethd G C 
-  \<equiv> (case class G C of
+definition
+  cdeclaredmethd :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,methd) table" where
+  "cdeclaredmethd G C =
+    (case class G C of
        None \<Rightarrow> \<lambda> sig. None
-     | Some c \<Rightarrow> table_of (methods c)
-    )"
+     | Some c \<Rightarrow> table_of (methods c))"
 
-definition cdeclaredfield :: "prog \<Rightarrow> qtname \<Rightarrow> (vname,field) table" where
-"cdeclaredfield G C 
-  \<equiv> (case class G C of
-       None \<Rightarrow> \<lambda> sig. None
-     | Some c \<Rightarrow> table_of (cfields c)
-    )"
+definition
+  cdeclaredfield :: "prog \<Rightarrow> qtname \<Rightarrow> (vname,field) table" where
+  "cdeclaredfield G C =
+    (case class G C of
+      None \<Rightarrow> \<lambda> sig. None
+    | Some c \<Rightarrow> table_of (cfields c))"
 
-definition declared_in :: "prog  \<Rightarrow> memberdecl \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile> _ declared'_in _" [61,61,61] 60) where
-"G\<turnstile>m declared_in C \<equiv> (case m of
-                        fdecl (fn,f ) \<Rightarrow> cdeclaredfield G C fn  = Some f
-                      | mdecl (sig,m) \<Rightarrow> cdeclaredmethd G C sig = Some m)"
+definition
+  declared_in :: "prog  \<Rightarrow> memberdecl \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile> _ declared'_in _" [61,61,61] 60)
+where
+  "G\<turnstile>m declared_in C = (case m of
+                          fdecl (fn,f ) \<Rightarrow> cdeclaredfield G C fn  = Some f
+                        | mdecl (sig,m) \<Rightarrow> cdeclaredmethd G C sig = Some m)"
 
 abbreviation
 method_declared_in:: "prog  \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool"
@@ -560,10 +578,12 @@
 by (cases m) 
    (auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def)
 
-definition undeclared_in :: "prog  \<Rightarrow> memberid \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile> _ undeclared'_in _" [61,61,61] 60) where
-"G\<turnstile>m undeclared_in C \<equiv> (case m of
-                            fid fn  \<Rightarrow> cdeclaredfield G C fn  = None
-                          | mid sig \<Rightarrow> cdeclaredmethd G C sig = None)"
+definition
+  undeclared_in :: "prog  \<Rightarrow> memberid \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile> _ undeclared'_in _" [61,61,61] 60)
+where
+  "G\<turnstile>m undeclared_in C = (case m of
+                           fid fn  \<Rightarrow> cdeclaredfield G C fn  = None
+                         | mid sig \<Rightarrow> cdeclaredmethd G C sig = None)"
 
 
 subsubsection "members"
@@ -607,17 +627,20 @@
                            ("_ \<turnstile>Field _  _ member'_of _" [61,61,61] 60)
  where "G\<turnstile>Field n f member_of C == G\<turnstile>fieldm n f member_of C"
 
-definition inherits :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> bool" ("_ \<turnstile> _ inherits _" [61,61,61] 60) where
-"G\<turnstile>C inherits m 
-  \<equiv> G\<turnstile>m inheritable_in (pid C) \<and> G\<turnstile>memberid m undeclared_in C \<and> 
-    (\<exists> S. G\<turnstile>C \<prec>\<^sub>C1 S \<and> G\<turnstile>(Class S) accessible_in (pid C) \<and> G\<turnstile>m member_of S)"
+definition
+  inherits :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> bool" ("_ \<turnstile> _ inherits _" [61,61,61] 60)
+where
+  "G\<turnstile>C inherits m =
+    (G\<turnstile>m inheritable_in (pid C) \<and> G\<turnstile>memberid m undeclared_in C \<and> 
+      (\<exists>S. G\<turnstile>C \<prec>\<^sub>C1 S \<and> G\<turnstile>(Class S) accessible_in (pid C) \<and> G\<turnstile>m member_of S))"
 
 lemma inherits_member: "G\<turnstile>C inherits m \<Longrightarrow> G\<turnstile>m member_of C"
 by (auto simp add: inherits_def intro: members.Inherited)
 
 
-definition member_in :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool" ("_ \<turnstile> _ member'_in _" [61,61,61] 60) where
-"G\<turnstile>m member_in C \<equiv> \<exists> provC. G\<turnstile> C \<preceq>\<^sub>C provC \<and> G \<turnstile> m member_of provC"
+definition
+  member_in :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool" ("_ \<turnstile> _ member'_in _" [61,61,61] 60)
+  where "G\<turnstile>m member_in C = (\<exists> provC. G\<turnstile> C \<preceq>\<^sub>C provC \<and> G \<turnstile> m member_of provC)"
 text {* A member is in a class if it is member of the class or a superclass.
 If a member is in a class we can select this member. This additional notion
 is necessary since not all members are inherited to subclasses. So such
@@ -703,13 +726,15 @@
 
 subsubsection "Hiding"
 
-definition hides :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" ("_\<turnstile> _ hides _" [61,61,61] 60) where 
-"G\<turnstile>new hides old
-  \<equiv> is_static new \<and> msig new = msig old \<and>
-    G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and>
-    G\<turnstile>Method new declared_in (declclass new) \<and>
-    G\<turnstile>Method old declared_in (declclass old) \<and> 
-    G\<turnstile>Method old inheritable_in pid (declclass new)"
+definition
+  hides :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" ("_\<turnstile> _ hides _" [61,61,61] 60)
+where 
+  "G\<turnstile>new hides old =
+    (is_static new \<and> msig new = msig old \<and>
+      G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and>
+      G\<turnstile>Method new declared_in (declclass new) \<and>
+      G\<turnstile>Method old declared_in (declclass old) \<and> 
+      G\<turnstile>Method old inheritable_in pid (declclass new))"
 
 abbreviation
 sig_hides:: "prog  \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool" 
@@ -762,16 +787,18 @@
 by (auto simp add: hides_def)
 
 subsubsection "permits access" 
-definition permits_acc :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" ("_ \<turnstile> _ in _ permits'_acc'_from _" [61,61,61,61] 60) where
-"G\<turnstile>membr in cls permits_acc_from accclass 
-  \<equiv> (case (accmodi membr) of
-       Private   \<Rightarrow> (declclass membr = accclass)
-     | Package   \<Rightarrow> (pid (declclass membr) = pid accclass)
-     | Protected \<Rightarrow> (pid (declclass membr) = pid accclass)
+definition
+  permits_acc :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" ("_ \<turnstile> _ in _ permits'_acc'_from _" [61,61,61,61] 60)
+where
+  "G\<turnstile>membr in cls permits_acc_from accclass =
+    (case (accmodi membr) of
+      Private   \<Rightarrow> (declclass membr = accclass)
+    | Package   \<Rightarrow> (pid (declclass membr) = pid accclass)
+    | Protected \<Rightarrow> (pid (declclass membr) = pid accclass)
                     \<or>
                     (G\<turnstile>accclass \<prec>\<^sub>C declclass membr 
                      \<and> (G\<turnstile>cls \<preceq>\<^sub>C accclass \<or> is_static membr)) 
-     | Public    \<Rightarrow> True)"
+    | Public    \<Rightarrow> True)"
 text {*
 The subcondition of the @{term "Protected"} case: 
 @{term "G\<turnstile>accclass \<prec>\<^sub>C declclass membr"} could also be relaxed to:
@@ -1380,24 +1407,25 @@
 translations 
   (type) "fspec" <= (type) "vname \<times> qtname" 
 
-definition imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
-"imethds G I 
-  \<equiv> iface_rec G I  
-              (\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus> 
+definition
+  imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
+  "imethds G I =
+    iface_rec G I  (\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus>
                         (Option.set \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
 text {* methods of an interface, with overriding and inheritance, cf. 9.2 *}
 
-definition accimethds :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
-"accimethds G pack I
-  \<equiv> if G\<turnstile>Iface I accessible_in pack 
-       then imethds G I
-       else (\<lambda> k. {})"
+definition
+  accimethds :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
+  "accimethds G pack I =
+    (if G\<turnstile>Iface I accessible_in pack 
+     then imethds G I
+     else (\<lambda> k. {}))"
 text {* only returns imethds if the interface is accessible *}
 
-definition methd :: "prog \<Rightarrow> qtname  \<Rightarrow> (sig,qtname \<times> methd) table" where
-
-"methd G C 
- \<equiv> class_rec G C empty
+definition
+  methd :: "prog \<Rightarrow> qtname  \<Rightarrow> (sig,qtname \<times> methd) table" where
+  "methd G C =
+    class_rec G C empty
              (\<lambda>C c subcls_mthds. 
                filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m)
                           subcls_mthds 
@@ -1409,10 +1437,10 @@
      Every new method with the same signature coalesces the
      method of a superclass. *}
 
-definition accmethd :: "prog \<Rightarrow> qtname \<Rightarrow> qtname  \<Rightarrow> (sig,qtname \<times> methd) table" where
-"accmethd G S C 
- \<equiv> filter_tab (\<lambda>sig m. G\<turnstile>method sig m of C accessible_from S) 
-              (methd G C)"
+definition
+  accmethd :: "prog \<Rightarrow> qtname \<Rightarrow> qtname  \<Rightarrow> (sig,qtname \<times> methd) table" where
+  "accmethd G S C =
+    filter_tab (\<lambda>sig m. G\<turnstile>method sig m of C accessible_from S) (methd G C)"
 text {* @{term "accmethd G S C"}: only those methods of @{term "methd G C"}, 
         accessible from S *}
 
@@ -1423,23 +1451,24 @@
     So we must test accessibility of method @{term m} of class @{term C} 
     (not @{term "declclass m"}) *}
 
-definition dynmethd :: "prog  \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
-"dynmethd G statC dynC  
-  \<equiv> \<lambda> sig. 
-     (if G\<turnstile>dynC \<preceq>\<^sub>C statC
-        then (case methd G statC sig of
-                None \<Rightarrow> None
-              | Some statM 
-                  \<Rightarrow> (class_rec G dynC empty
-                       (\<lambda>C c subcls_mthds. 
-                          subcls_mthds
-                          ++
-                          (filter_tab 
-                            (\<lambda> _ dynM. G,sig\<turnstile>dynM overrides statM \<or> dynM=statM)
-                            (methd G C) ))
-                      ) sig
-              )
-        else None)"
+definition
+  dynmethd :: "prog  \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
+  "dynmethd G statC dynC =
+    (\<lambda>sig.
+       (if G\<turnstile>dynC \<preceq>\<^sub>C statC
+          then (case methd G statC sig of
+                  None \<Rightarrow> None
+                | Some statM 
+                    \<Rightarrow> (class_rec G dynC empty
+                         (\<lambda>C c subcls_mthds. 
+                            subcls_mthds
+                            ++
+                            (filter_tab 
+                              (\<lambda> _ dynM. G,sig\<turnstile>dynM overrides statM \<or> dynM=statM)
+                              (methd G C) ))
+                        ) sig
+                )
+          else None))"
 
 text {* @{term "dynmethd G statC dynC"}: dynamic method lookup of a reference 
         with dynamic class @{term dynC} and static class @{term statC} *}
@@ -1449,11 +1478,12 @@
         filters the new methods (to get only those methods which actually
         override the methods of the static class) *}
 
-definition dynimethd :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
-"dynimethd G I dynC 
-  \<equiv> \<lambda> sig. if imethds G I sig \<noteq> {}
-               then methd G dynC sig
-               else dynmethd G Object dynC sig"
+definition
+  dynimethd :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
+  "dynimethd G I dynC =
+    (\<lambda>sig. if imethds G I sig \<noteq> {}
+           then methd G dynC sig
+           else dynmethd G Object dynC sig)"
 text {* @{term "dynimethd G I dynC"}: dynamic method lookup of a reference with 
         dynamic class dynC and static interface type I *}
 text {* 
@@ -1468,31 +1498,34 @@
    down to the actual dynamic class.
  *}
 
-definition dynlookup :: "prog  \<Rightarrow> ref_ty \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
-"dynlookup G statT dynC
-  \<equiv> (case statT of
-       NullT        \<Rightarrow> empty
-     | IfaceT I     \<Rightarrow> dynimethd G I      dynC
-     | ClassT statC \<Rightarrow> dynmethd  G statC  dynC
-     | ArrayT ty    \<Rightarrow> dynmethd  G Object dynC)"
+definition
+  dynlookup :: "prog  \<Rightarrow> ref_ty \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
+  "dynlookup G statT dynC =
+    (case statT of
+      NullT        \<Rightarrow> empty
+    | IfaceT I     \<Rightarrow> dynimethd G I      dynC
+    | ClassT statC \<Rightarrow> dynmethd  G statC  dynC
+    | ArrayT ty    \<Rightarrow> dynmethd  G Object dynC)"
 text {* @{term "dynlookup G statT dynC"}: dynamic lookup of a method within the 
     static reference type statT and the dynamic class dynC. 
     In a wellformd context statT will not be NullT and in case
     statT is an array type, dynC=Object *}
 
-definition fields :: "prog \<Rightarrow> qtname \<Rightarrow> ((vname \<times> qtname) \<times> field) list" where
-"fields G C 
-  \<equiv> class_rec G C [] (\<lambda>C c ts. map (\<lambda>(n,t). ((n,C),t)) (cfields c) @ ts)"
+definition
+  fields :: "prog \<Rightarrow> qtname \<Rightarrow> ((vname \<times> qtname) \<times> field) list" where
+  "fields G C =
+    class_rec G C [] (\<lambda>C c ts. map (\<lambda>(n,t). ((n,C),t)) (cfields c) @ ts)"
 text {* @{term "fields G C"} 
      list of fields of a class, including all the fields of the superclasses
      (private, inherited and hidden ones) not only the accessible ones
      (an instance of a object allocates all these fields *}
 
-definition accfield :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (vname, qtname  \<times>  field) table" where
-"accfield G S C
-  \<equiv> let field_tab = table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (fields G C))
-    in filter_tab (\<lambda>n (declC,f). G\<turnstile> (declC,fdecl (n,f)) of C accessible_from S)
-                  field_tab"
+definition
+  accfield :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (vname, qtname  \<times>  field) table" where
+  "accfield G S C =
+    (let field_tab = table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (fields G C))
+      in filter_tab (\<lambda>n (declC,f). G\<turnstile> (declC,fdecl (n,f)) of C accessible_from S)
+                    field_tab)"
 text  {* @{term "accfield G C S"}: fields of a class @{term C} which are 
          accessible from scope of class
          @{term S} with inheritance and hiding, cf. 8.3 *}
@@ -1503,11 +1536,13 @@
    inheritance, too. So we must test accessibility of field @{term f} of class 
    @{term C} (not @{term "declclass f"}) *} 
 
-definition is_methd :: "prog \<Rightarrow> qtname  \<Rightarrow> sig \<Rightarrow> bool" where
- "is_methd G \<equiv> \<lambda>C sig. is_class G C \<and> methd G C sig \<noteq> None"
+definition
+  is_methd :: "prog \<Rightarrow> qtname  \<Rightarrow> sig \<Rightarrow> bool"
+  where "is_methd G = (\<lambda>C sig. is_class G C \<and> methd G C sig \<noteq> None)"
 
-definition efname :: "((vname \<times> qtname) \<times> field) \<Rightarrow> (vname \<times> qtname)" where
-"efname \<equiv> fst"
+definition
+  efname :: "((vname \<times> qtname) \<times> field) \<Rightarrow> (vname \<times> qtname)"
+  where "efname = fst"
 
 lemma efname_simp[simp]:"efname (n,f) = n"
 by (simp add: efname_def) 
@@ -2270,8 +2305,9 @@
 
 section "calculation of the superclasses of a class"
 
-definition superclasses :: "prog \<Rightarrow> qtname \<Rightarrow> qtname set" where
- "superclasses G C \<equiv> class_rec G C {} 
+definition
+  superclasses :: "prog \<Rightarrow> qtname \<Rightarrow> qtname set" where
+ "superclasses G C = class_rec G C {} 
                        (\<lambda> C c superclss. (if C=Object 
                                             then {} 
                                             else insert (super c) superclss))"
diff -r d9549f9da779 -r a79abb22ca9c src/HOL/Bali/DefiniteAssignment.thy
--- a/src/HOL/Bali/DefiniteAssignment.thy	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/DefiniteAssignment.thy	Mon Jul 26 18:25:19 2010 +0200
@@ -49,33 +49,33 @@
 with a jump, since no breaks, continues or returns are allowed in an 
 expression. *}
 
-consts jumpNestingOkS :: "jump set \<Rightarrow> stmt \<Rightarrow> bool"
-primrec
-"jumpNestingOkS jmps (Skip)   = True"
-"jumpNestingOkS jmps (Expr e) = True"
-"jumpNestingOkS jmps (j\<bullet> s) = jumpNestingOkS ({j} \<union> jmps) s"
-"jumpNestingOkS jmps (c1;;c2) = (jumpNestingOkS jmps c1 \<and> 
-                                 jumpNestingOkS jmps c2)"
-"jumpNestingOkS jmps (If(e) c1 Else c2) = (jumpNestingOkS jmps c1 \<and>  
-                                           jumpNestingOkS jmps c2)"
-"jumpNestingOkS jmps (l\<bullet> While(e) c) = jumpNestingOkS ({Cont l} \<union> jmps) c"
+primrec jumpNestingOkS :: "jump set \<Rightarrow> stmt \<Rightarrow> bool"
+where
+  "jumpNestingOkS jmps (Skip)   = True"
+| "jumpNestingOkS jmps (Expr e) = True"
+| "jumpNestingOkS jmps (j\<bullet> s) = jumpNestingOkS ({j} \<union> jmps) s"
+| "jumpNestingOkS jmps (c1;;c2) = (jumpNestingOkS jmps c1 \<and> 
+                                   jumpNestingOkS jmps c2)"
+| "jumpNestingOkS jmps (If(e) c1 Else c2) = (jumpNestingOkS jmps c1 \<and>  
+                                             jumpNestingOkS jmps c2)"
+| "jumpNestingOkS jmps (l\<bullet> While(e) c) = jumpNestingOkS ({Cont l} \<union> jmps) c"
 --{* The label of the while loop only handles continue jumps. Breaks are only
      handled by @{term Lab} *}
-"jumpNestingOkS jmps (Jmp j) = (j \<in> jmps)"
-"jumpNestingOkS jmps (Throw e) = True"
-"jumpNestingOkS jmps (Try c1 Catch(C vn) c2) = (jumpNestingOkS jmps c1 \<and> 
-                                                jumpNestingOkS jmps c2)"
-"jumpNestingOkS jmps (c1 Finally c2) = (jumpNestingOkS jmps c1 \<and> 
-                                        jumpNestingOkS jmps c2)"
-"jumpNestingOkS jmps (Init C) = True" 
+| "jumpNestingOkS jmps (Jmp j) = (j \<in> jmps)"
+| "jumpNestingOkS jmps (Throw e) = True"
+| "jumpNestingOkS jmps (Try c1 Catch(C vn) c2) = (jumpNestingOkS jmps c1 \<and> 
+                                                  jumpNestingOkS jmps c2)"
+| "jumpNestingOkS jmps (c1 Finally c2) = (jumpNestingOkS jmps c1 \<and> 
+                                          jumpNestingOkS jmps c2)"
+| "jumpNestingOkS jmps (Init C) = True" 
  --{* wellformedness of the program must enshure that for all initializers 
       jumpNestingOkS {} holds *} 
 --{* Dummy analysis for intermediate smallstep term @{term  FinA} *}
-"jumpNestingOkS jmps (FinA a c) = False"
+| "jumpNestingOkS jmps (FinA a c) = False"
 
 
 definition jumpNestingOk :: "jump set \<Rightarrow> term \<Rightarrow> bool" where
-"jumpNestingOk jmps t \<equiv> (case t of
+"jumpNestingOk jmps t = (case t of
                       In1 se \<Rightarrow> (case se of
                                    Inl e \<Rightarrow> True
                                  | Inr s \<Rightarrow> jumpNestingOkS jmps s)
@@ -116,48 +116,46 @@
 
 subsection {* Very restricted calculation fallback calculation *}
 
-consts the_LVar_name:: "var \<Rightarrow> lname"
-primrec 
-"the_LVar_name (LVar n) = n"
+primrec the_LVar_name :: "var \<Rightarrow> lname"
+  where "the_LVar_name (LVar n) = n"
 
-consts assignsE :: "expr      \<Rightarrow> lname set" 
-       assignsV :: "var       \<Rightarrow> lname set"
-       assignsEs:: "expr list \<Rightarrow> lname set"
-text {* *}
-primrec
-"assignsE (NewC c)            = {}" 
-"assignsE (NewA t e)          = assignsE e"
-"assignsE (Cast t e)          = assignsE e"
-"assignsE (e InstOf r)        = assignsE e"
-"assignsE (Lit val)           = {}"
-"assignsE (UnOp unop e)       = assignsE e"
-"assignsE (BinOp binop e1 e2) = (if binop=CondAnd \<or> binop=CondOr
-                                     then (assignsE e1)
-                                     else (assignsE e1) \<union> (assignsE e2))" 
-"assignsE (Super)             = {}"
-"assignsE (Acc v)             = assignsV v"
-"assignsE (v:=e)              = (assignsV v) \<union> (assignsE e) \<union> 
-                                 (if \<exists> n. v=(LVar n) then {the_LVar_name v} 
-                                                     else {})"
-"assignsE (b? e1 : e2) = (assignsE b) \<union> ((assignsE e1) \<inter> (assignsE e2))"
-"assignsE ({accC,statT,mode}objRef\<cdot>mn({pTs}args)) 
-                          = (assignsE objRef) \<union> (assignsEs args)"
+primrec assignsE :: "expr \<Rightarrow> lname set" 
+  and assignsV :: "var \<Rightarrow> lname set"
+  and assignsEs:: "expr list \<Rightarrow> lname set"
+where
+  "assignsE (NewC c)            = {}" 
+| "assignsE (NewA t e)          = assignsE e"
+| "assignsE (Cast t e)          = assignsE e"
+| "assignsE (e InstOf r)        = assignsE e"
+| "assignsE (Lit val)           = {}"
+| "assignsE (UnOp unop e)       = assignsE e"
+| "assignsE (BinOp binop e1 e2) = (if binop=CondAnd \<or> binop=CondOr
+                                       then (assignsE e1)
+                                       else (assignsE e1) \<union> (assignsE e2))" 
+| "assignsE (Super)             = {}"
+| "assignsE (Acc v)             = assignsV v"
+| "assignsE (v:=e)              = (assignsV v) \<union> (assignsE e) \<union> 
+                                   (if \<exists> n. v=(LVar n) then {the_LVar_name v} 
+                                                       else {})"
+| "assignsE (b? e1 : e2) = (assignsE b) \<union> ((assignsE e1) \<inter> (assignsE e2))"
+| "assignsE ({accC,statT,mode}objRef\<cdot>mn({pTs}args)) 
+                            = (assignsE objRef) \<union> (assignsEs args)"
 -- {* Only dummy analysis for intermediate expressions  
       @{term Methd}, @{term Body}, @{term InsInitE} and @{term Callee} *}
-"assignsE (Methd C sig)   = {}" 
-"assignsE (Body  C s)     = {}"   
-"assignsE (InsInitE s e)  = {}"  
-"assignsE (Callee l e)    = {}" 
+| "assignsE (Methd C sig)   = {}" 
+| "assignsE (Body  C s)     = {}"   
+| "assignsE (InsInitE s e)  = {}"  
+| "assignsE (Callee l e)    = {}" 
 
-"assignsV (LVar n)       = {}"
-"assignsV ({accC,statDeclC,stat}objRef..fn) = assignsE objRef"
-"assignsV (e1.[e2])      = assignsE e1 \<union> assignsE e2"
+| "assignsV (LVar n)       = {}"
+| "assignsV ({accC,statDeclC,stat}objRef..fn) = assignsE objRef"
+| "assignsV (e1.[e2])      = assignsE e1 \<union> assignsE e2"
 
-"assignsEs     [] = {}"
-"assignsEs (e#es) = assignsE e \<union> assignsEs es"
+| "assignsEs     [] = {}"
+| "assignsEs (e#es) = assignsE e \<union> assignsEs es"
 
 definition assigns :: "term \<Rightarrow> lname set" where
-"assigns t \<equiv> (case t of
+"assigns t = (case t of
                 In1 se \<Rightarrow> (case se of
                              Inl e \<Rightarrow> assignsE e
                            | Inr s \<Rightarrow> {})
@@ -190,42 +188,42 @@
 
 subsection "Analysis of constant expressions"
 
-consts constVal :: "expr \<Rightarrow> val option"
-primrec 
-"constVal (NewC c)      = None"
-"constVal (NewA t e)    = None"
-"constVal (Cast t e)    = None"
-"constVal (Inst e r)    = None"
-"constVal (Lit val)     = Some val"
-"constVal (UnOp unop e) = (case (constVal e) of
-                             None   \<Rightarrow> None
-                           | Some v \<Rightarrow> Some (eval_unop unop v))" 
-"constVal (BinOp binop e1 e2) = (case (constVal e1) of
-                                   None    \<Rightarrow> None
-                                 | Some v1 \<Rightarrow> (case (constVal e2) of 
-                                                None    \<Rightarrow> None
-                                              | Some v2 \<Rightarrow> Some (eval_binop 
-                                                                 binop v1 v2)))"
-"constVal (Super)         = None"
-"constVal (Acc v)         = None"
-"constVal (Ass v e)       = None"
-"constVal (Cond b e1 e2)  = (case (constVal b) of
+primrec constVal :: "expr \<Rightarrow> val option"
+where
+  "constVal (NewC c)      = None"
+| "constVal (NewA t e)    = None"
+| "constVal (Cast t e)    = None"
+| "constVal (Inst e r)    = None"
+| "constVal (Lit val)     = Some val"
+| "constVal (UnOp unop e) = (case (constVal e) of
                                None   \<Rightarrow> None
-                             | Some bv\<Rightarrow> (case the_Bool bv of
-                                            True \<Rightarrow> (case (constVal e2) of
-                                                       None   \<Rightarrow> None
-                                                     | Some v \<Rightarrow> constVal e1)
-                                          | False\<Rightarrow> (case (constVal e1) of
-                                                       None   \<Rightarrow> None
-                                                     | Some v \<Rightarrow> constVal e2)))"
+                             | Some v \<Rightarrow> Some (eval_unop unop v))" 
+| "constVal (BinOp binop e1 e2) = (case (constVal e1) of
+                                     None    \<Rightarrow> None
+                                   | Some v1 \<Rightarrow> (case (constVal e2) of 
+                                                  None    \<Rightarrow> None
+                                                | Some v2 \<Rightarrow> Some (eval_binop 
+                                                                   binop v1 v2)))"
+| "constVal (Super)         = None"
+| "constVal (Acc v)         = None"
+| "constVal (Ass v e)       = None"
+| "constVal (Cond b e1 e2)  = (case (constVal b) of
+                                 None   \<Rightarrow> None
+                               | Some bv\<Rightarrow> (case the_Bool bv of
+                                              True \<Rightarrow> (case (constVal e2) of
+                                                         None   \<Rightarrow> None
+                                                       | Some v \<Rightarrow> constVal e1)
+                                            | False\<Rightarrow> (case (constVal e1) of
+                                                         None   \<Rightarrow> None
+                                                       | Some v \<Rightarrow> constVal e2)))"
 --{* Note that @{text "constVal (Cond b e1 e2)"} is stricter as it could be.
      It requires that all tree expressions are constant even if we can decide
      which branch to choose, provided the constant value of @{term b} *}
-"constVal (Call accC statT mode objRef mn pTs args) = None"
-"constVal (Methd C sig)   = None" 
-"constVal (Body  C s)     = None"   
-"constVal (InsInitE s e)  = None"  
-"constVal (Callee l e)    = None" 
+| "constVal (Call accC statT mode objRef mn pTs args) = None"
+| "constVal (Methd C sig)   = None" 
+| "constVal (Body  C s)     = None"   
+| "constVal (InsInitE s e)  = None"  
+| "constVal (Callee l e)    = None" 
 
 lemma constVal_Some_induct [consumes 1, case_names Lit UnOp BinOp CondL CondR]: 
   assumes const: "constVal e = Some v" and
@@ -282,55 +280,55 @@
 to a specific boolean value. If the expression cannot evaluate to a 
 @{term Boolean} value UNIV is returned. If we expect true/false the opposite 
 constant false/true will also lead to UNIV. *}
-consts assigns_if:: "bool \<Rightarrow> expr \<Rightarrow> lname set" 
-primrec
-"assigns_if b (NewC c)            = UNIV" --{*can never evaluate to Boolean*} 
-"assigns_if b (NewA t e)          = UNIV" --{*can never evaluate to Boolean*}
-"assigns_if b (Cast t e)          = assigns_if b e" 
-"assigns_if b (Inst e r)          = assignsE e" --{*Inst has type Boolean but
-                                                     e is a reference type*}
-"assigns_if b (Lit val)           = (if val=Bool b then {} else UNIV)"  
-"assigns_if b (UnOp unop e)       = (case constVal (UnOp unop e) of
-                                         None   \<Rightarrow> (if unop = UNot 
-                                                       then assigns_if (\<not>b) e
-                                                       else UNIV)
-                                       | Some v \<Rightarrow> (if v=Bool b 
-                                                       then {} 
-                                                       else UNIV))"
-"assigns_if b (BinOp binop e1 e2) 
-  = (case constVal (BinOp binop e1 e2) of
-       None \<Rightarrow> (if binop=CondAnd then
-                   (case b of 
-                       True  \<Rightarrow> assigns_if True  e1 \<union> assigns_if True e2
-                    |  False \<Rightarrow> assigns_if False e1 \<inter> 
-                                (assigns_if True e1 \<union> assigns_if False e2))
-                else
-               (if binop=CondOr then
-                   (case b of 
-                       True  \<Rightarrow> assigns_if True e1 \<inter> 
-                                (assigns_if False e1 \<union> assigns_if True e2)
-                    |  False \<Rightarrow> assigns_if False  e1 \<union> assigns_if False e2)
-                else assignsE e1 \<union> assignsE e2))
-     | Some v \<Rightarrow> (if v=Bool b then {} else UNIV))"
+primrec assigns_if :: "bool \<Rightarrow> expr \<Rightarrow> lname set"
+where
+  "assigns_if b (NewC c)            = UNIV" --{*can never evaluate to Boolean*} 
+| "assigns_if b (NewA t e)          = UNIV" --{*can never evaluate to Boolean*}
+| "assigns_if b (Cast t e)          = assigns_if b e" 
+| "assigns_if b (Inst e r)          = assignsE e" --{*Inst has type Boolean but
+                                                       e is a reference type*}
+| "assigns_if b (Lit val)           = (if val=Bool b then {} else UNIV)"  
+| "assigns_if b (UnOp unop e)       = (case constVal (UnOp unop e) of
+                                           None   \<Rightarrow> (if unop = UNot 
+                                                         then assigns_if (\<not>b) e
+                                                         else UNIV)
+                                         | Some v \<Rightarrow> (if v=Bool b 
+                                                         then {} 
+                                                         else UNIV))"
+| "assigns_if b (BinOp binop e1 e2) 
+    = (case constVal (BinOp binop e1 e2) of
+         None \<Rightarrow> (if binop=CondAnd then
+                     (case b of 
+                         True  \<Rightarrow> assigns_if True  e1 \<union> assigns_if True e2
+                      |  False \<Rightarrow> assigns_if False e1 \<inter> 
+                                  (assigns_if True e1 \<union> assigns_if False e2))
+                  else
+                 (if binop=CondOr then
+                     (case b of 
+                         True  \<Rightarrow> assigns_if True e1 \<inter> 
+                                  (assigns_if False e1 \<union> assigns_if True e2)
+                      |  False \<Rightarrow> assigns_if False  e1 \<union> assigns_if False e2)
+                  else assignsE e1 \<union> assignsE e2))
+       | Some v \<Rightarrow> (if v=Bool b then {} else UNIV))"
 
-"assigns_if b (Super)      = UNIV" --{*can never evaluate to Boolean*}
-"assigns_if b (Acc v)      = (assignsV v)"
-"assigns_if b (v := e)     = (assignsE (Ass v e))"
-"assigns_if b (c? e1 : e2) = (assignsE c) \<union>
-                               (case (constVal c) of
-                                  None    \<Rightarrow> (assigns_if b e1) \<inter> 
-                                             (assigns_if b e2)
-                                | Some bv \<Rightarrow> (case the_Bool bv of
-                                                True  \<Rightarrow> assigns_if b e1
-                                              | False \<Rightarrow> assigns_if b e2))"
-"assigns_if b ({accC,statT,mode}objRef\<cdot>mn({pTs}args))  
-          = assignsE ({accC,statT,mode}objRef\<cdot>mn({pTs}args)) "
+| "assigns_if b (Super)      = UNIV" --{*can never evaluate to Boolean*}
+| "assigns_if b (Acc v)      = (assignsV v)"
+| "assigns_if b (v := e)     = (assignsE (Ass v e))"
+| "assigns_if b (c? e1 : e2) = (assignsE c) \<union>
+                                 (case (constVal c) of
+                                    None    \<Rightarrow> (assigns_if b e1) \<inter> 
+                                               (assigns_if b e2)
+                                  | Some bv \<Rightarrow> (case the_Bool bv of
+                                                  True  \<Rightarrow> assigns_if b e1
+                                                | False \<Rightarrow> assigns_if b e2))"
+| "assigns_if b ({accC,statT,mode}objRef\<cdot>mn({pTs}args))  
+            = assignsE ({accC,statT,mode}objRef\<cdot>mn({pTs}args)) "
 -- {* Only dummy analysis for intermediate expressions  
       @{term Methd}, @{term Body}, @{term InsInitE} and @{term Callee} *}
-"assigns_if b (Methd C sig)   = {}" 
-"assigns_if b (Body  C s)     = {}"   
-"assigns_if b (InsInitE s e)  = {}"  
-"assigns_if b (Callee l e)    = {}" 
+| "assigns_if b (Methd C sig)   = {}" 
+| "assigns_if b (Body  C s)     = {}"   
+| "assigns_if b (InsInitE s e)  = {}"  
+| "assigns_if b (Callee l e)    = {}" 
 
 lemma assigns_if_const_b_simp:
   assumes boolConst: "constVal e = Some (Bool b)" (is "?Const b e")
@@ -429,14 +427,17 @@
 
 subsection {* Lifting set operations to range of tables (map to a set) *}
 
-definition union_ts :: "('a,'b) tables \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables" ("_ \<Rightarrow>\<union> _" [67,67] 65) where
- "A \<Rightarrow>\<union> B \<equiv> \<lambda> k. A k \<union> B k"
+definition
+  union_ts :: "('a,'b) tables \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables" ("_ \<Rightarrow>\<union> _" [67,67] 65)
+  where "A \<Rightarrow>\<union> B = (\<lambda> k. A k \<union> B k)"
 
-definition intersect_ts :: "('a,'b) tables \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables" ("_ \<Rightarrow>\<inter>  _" [72,72] 71) where
- "A \<Rightarrow>\<inter>  B \<equiv> \<lambda> k. A k \<inter> B k"
+definition
+  intersect_ts :: "('a,'b) tables \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables" ("_ \<Rightarrow>\<inter>  _" [72,72] 71)
+  where "A \<Rightarrow>\<inter>  B = (\<lambda>k. A k \<inter> B k)"
 
-definition all_union_ts :: "('a,'b) tables \<Rightarrow> 'b set \<Rightarrow> ('a,'b) tables" (infixl "\<Rightarrow>\<union>\<^sub>\<forall>" 40) where 
- "A \<Rightarrow>\<union>\<^sub>\<forall> B \<equiv> \<lambda> k. A k \<union> B"
+definition
+  all_union_ts :: "('a,'b) tables \<Rightarrow> 'b set \<Rightarrow> ('a,'b) tables" (infixl "\<Rightarrow>\<union>\<^sub>\<forall>" 40)
+  where "(A \<Rightarrow>\<union>\<^sub>\<forall> B) = (\<lambda> k. A k \<union> B)"
   
 subsubsection {* Binary union of tables *}
 
@@ -507,16 +508,19 @@
          brk :: "breakass" --{* Definetly assigned variables for 
                                 abrupt completion with a break *}
 
-definition rmlab :: "'a \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables" where
-"rmlab k A \<equiv> \<lambda> x. if x=k then UNIV else A x"
+definition
+  rmlab :: "'a \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables"
+  where "rmlab k A = (\<lambda>x. if x=k then UNIV else A x)"
  
 (*
-definition setbrk :: "breakass \<Rightarrow> assigned \<Rightarrow> breakass set" where
-"setbrk b A \<equiv> {b} \<union> {a| a. a\<in> brk A \<and> lab a \<noteq> lab b}"
+definition
+  setbrk :: "breakass \<Rightarrow> assigned \<Rightarrow> breakass set" where
+  "setbrk b A = {b} \<union> {a| a. a\<in> brk A \<and> lab a \<noteq> lab b}"
 *)
 
-definition range_inter_ts :: "('a,'b) tables \<Rightarrow> 'b set" ("\<Rightarrow>\<Inter>_" 80) where 
- "\<Rightarrow>\<Inter>A \<equiv> {x |x. \<forall> k. x \<in> A k}"
+definition
+  range_inter_ts :: "('a,'b) tables \<Rightarrow> 'b set" ("\<Rightarrow>\<Inter>_" 80)
+  where "\<Rightarrow>\<Inter>A = {x |x. \<forall> k. x \<in> A k}"
 
 text {*
 In @{text "E\<turnstile> B \<guillemotright>t\<guillemotright> A"},
diff -r d9549f9da779 -r a79abb22ca9c src/HOL/Bali/Eval.thy
--- a/src/HOL/Bali/Eval.thy	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/Eval.thy	Mon Jul 26 18:25:19 2010 +0200
@@ -141,7 +141,7 @@
   where "\<lfloor>es\<rfloor>\<^sub>l == In3 es"
 
 definition undefined3 :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> vals" where
- "undefined3 \<equiv> sum3_case (In1 \<circ> sum_case (\<lambda>x. undefined) (\<lambda>x. Unit))
+ "undefined3 = sum3_case (In1 \<circ> sum_case (\<lambda>x. undefined) (\<lambda>x. Unit))
                      (\<lambda>x. In2 undefined) (\<lambda>x. In3 undefined)"
 
 lemma [simp]: "undefined3 (In1l x) = In1 undefined"
@@ -159,8 +159,9 @@
 
 section "exception throwing and catching"
 
-definition throw :: "val \<Rightarrow> abopt \<Rightarrow> abopt" where
- "throw a' x \<equiv> abrupt_if True (Some (Xcpt (Loc (the_Addr a')))) (np a' x)"
+definition
+  throw :: "val \<Rightarrow> abopt \<Rightarrow> abopt" where
+  "throw a' x = abrupt_if True (Some (Xcpt (Loc (the_Addr a')))) (np a' x)"
 
 lemma throw_def2: 
  "throw a' x = abrupt_if True (Some (Xcpt (Loc (the_Addr a')))) (np a' x)"
@@ -168,8 +169,9 @@
 apply (simp (no_asm))
 done
 
-definition fits :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_ fits _"[61,61,61,61]60) where
- "G,s\<turnstile>a' fits T  \<equiv> (\<exists>rt. T=RefT rt) \<longrightarrow> a'=Null \<or> G\<turnstile>obj_ty(lookup_obj s a')\<preceq>T"
+definition
+  fits :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_ fits _"[61,61,61,61]60)
+  where "G,s\<turnstile>a' fits T = ((\<exists>rt. T=RefT rt) \<longrightarrow> a'=Null \<or> G\<turnstile>obj_ty(lookup_obj s a')\<preceq>T)"
 
 lemma fits_Null [simp]: "G,s\<turnstile>Null fits T"
 by (simp add: fits_def)
@@ -192,9 +194,10 @@
 apply iprover
 done
 
-definition catch :: "prog \<Rightarrow> state \<Rightarrow> qtname \<Rightarrow> bool" ("_,_\<turnstile>catch _"[61,61,61]60) where
- "G,s\<turnstile>catch C\<equiv>\<exists>xc. abrupt s=Some (Xcpt xc) \<and> 
-                    G,store s\<turnstile>Addr (the_Loc xc) fits Class C"
+definition
+  catch :: "prog \<Rightarrow> state \<Rightarrow> qtname \<Rightarrow> bool" ("_,_\<turnstile>catch _"[61,61,61]60) where
+  "G,s\<turnstile>catch C = (\<exists>xc. abrupt s=Some (Xcpt xc) \<and> 
+                        G,store s\<turnstile>Addr (the_Loc xc) fits Class C)"
 
 lemma catch_Norm [simp]: "\<not>G,Norm s\<turnstile>catch tn"
 apply (unfold catch_def)
@@ -217,9 +220,9 @@
 apply (simp (no_asm))
 done
 
-definition new_xcpt_var :: "vname \<Rightarrow> state \<Rightarrow> state" where
- "new_xcpt_var vn \<equiv> 
-     \<lambda>(x,s). Norm (lupd(VName vn\<mapsto>Addr (the_Loc (the_Xcpt (the x)))) s)"
+definition
+  new_xcpt_var :: "vname \<Rightarrow> state \<Rightarrow> state" where
+  "new_xcpt_var vn = (\<lambda>(x,s). Norm (lupd(VName vn\<mapsto>Addr (the_Loc (the_Xcpt (the x)))) s))"
 
 lemma new_xcpt_var_def2 [simp]: 
  "new_xcpt_var vn (x,s) = 
@@ -232,9 +235,10 @@
 
 section "misc"
 
-definition assign :: "('a \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> 'a \<Rightarrow> state \<Rightarrow> state" where
- "assign f v \<equiv> \<lambda>(x,s). let (x',s') = (if x = None then f v else id) (x,s)
-                   in  (x',if x' = None then s' else s)"
+definition
+  assign :: "('a \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> 'a \<Rightarrow> state \<Rightarrow> state" where
+ "assign f v = (\<lambda>(x,s). let (x',s') = (if x = None then f v else id) (x,s)
+                        in  (x',if x' = None then s' else s))"
 
 (*
 lemma assign_Norm_Norm [simp]: 
@@ -293,26 +297,29 @@
 done
 *)
 
-definition init_comp_ty :: "ty \<Rightarrow> stmt" where
- "init_comp_ty T \<equiv> if (\<exists>C. T = Class C) then Init (the_Class T) else Skip"
+definition
+  init_comp_ty :: "ty \<Rightarrow> stmt"
+  where "init_comp_ty T = (if (\<exists>C. T = Class C) then Init (the_Class T) else Skip)"
 
 lemma init_comp_ty_PrimT [simp]: "init_comp_ty (PrimT pt) = Skip"
 apply (unfold init_comp_ty_def)
 apply (simp (no_asm))
 done
 
-definition invocation_class :: "inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> qtname" where
- "invocation_class m s a' statT 
-    \<equiv> (case m of
-         Static \<Rightarrow> if (\<exists> statC. statT = ClassT statC) 
-                      then the_Class (RefT statT) 
-                      else Object
-       | SuperM \<Rightarrow> the_Class (RefT statT)
-       | IntVir \<Rightarrow> obj_class (lookup_obj s a'))"
+definition
+  invocation_class :: "inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> qtname" where
+ "invocation_class m s a' statT =
+    (case m of
+       Static \<Rightarrow> if (\<exists> statC. statT = ClassT statC) 
+                    then the_Class (RefT statT) 
+                    else Object
+     | SuperM \<Rightarrow> the_Class (RefT statT)
+     | IntVir \<Rightarrow> obj_class (lookup_obj s a'))"
 
-definition invocation_declclass::"prog \<Rightarrow> inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> qtname" where
-"invocation_declclass G m s a' statT sig 
-   \<equiv> declclass (the (dynlookup G statT 
+definition
+  invocation_declclass :: "prog \<Rightarrow> inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> qtname" where
+  "invocation_declclass G m s a' statT sig =
+    declclass (the (dynlookup G statT
                                 (invocation_class m s a' statT)
                                 sig))" 
   
@@ -330,10 +337,11 @@
                                             else Object)"
 by (simp add: invocation_class_def)
 
-definition init_lvars :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> inv_mode \<Rightarrow> val \<Rightarrow> val list \<Rightarrow>
-                   state \<Rightarrow> state" where
- "init_lvars G C sig mode a' pvs 
-   \<equiv> \<lambda> (x,s). 
+definition
+  init_lvars :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> inv_mode \<Rightarrow> val \<Rightarrow> val list \<Rightarrow> state \<Rightarrow> state"
+where
+  "init_lvars G C sig mode a' pvs =
+    (\<lambda>(x,s). 
       let m = mthd (the (methd G C sig));
           l = \<lambda> k. 
               (case k of
@@ -343,7 +351,7 @@
                        | Res    \<Rightarrow> None)
                | This 
                    \<Rightarrow> (if mode=Static then None else Some a'))
-      in set_lvars l (if mode = Static then x else np a' x,s)"
+      in set_lvars l (if mode = Static then x else np a' x,s))"
 
 
 
@@ -364,9 +372,11 @@
 apply (simp (no_asm) add: Let_def)
 done
 
-definition body :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> expr" where
- "body G C sig \<equiv> let m = the (methd G C sig) 
-                 in Body (declclass m) (stmt (mbody (mthd m)))"
+definition
+  body :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> expr" where
+ "body G C sig =
+    (let m = the (methd G C sig) 
+     in Body (declclass m) (stmt (mbody (mthd m))))"
 
 lemma body_def2: --{* better suited for simplification *} 
 "body G C sig = Body  (declclass (the (methd G C sig))) 
@@ -377,28 +387,30 @@
 
 section "variables"
 
-definition lvar :: "lname \<Rightarrow> st \<Rightarrow> vvar" where
- "lvar vn s \<equiv> (the (locals s vn), \<lambda>v. supd (lupd(vn\<mapsto>v)))"
+definition
+  lvar :: "lname \<Rightarrow> st \<Rightarrow> vvar"
+  where "lvar vn s = (the (locals s vn), \<lambda>v. supd (lupd(vn\<mapsto>v)))"
 
-definition fvar :: "qtname \<Rightarrow> bool \<Rightarrow> vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state" where
- "fvar C stat fn a' s 
-    \<equiv> let (oref,xf) = if stat then (Stat C,id)
-                              else (Heap (the_Addr a'),np a');
+definition
+  fvar :: "qtname \<Rightarrow> bool \<Rightarrow> vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state" where
+ "fvar C stat fn a' s =
+   (let (oref,xf) = if stat then (Stat C,id)
+                            else (Heap (the_Addr a'),np a');
                   n = Inl (fn,C); 
                   f = (\<lambda>v. supd (upd_gobj oref n v)) 
-      in ((the (values (the (globs (store s) oref)) n),f),abupd xf s)"
+    in ((the (values (the (globs (store s) oref)) n),f),abupd xf s))"
 
-definition avar :: "prog \<Rightarrow> val \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state" where
- "avar G i' a' s 
-    \<equiv> let   oref = Heap (the_Addr a'); 
-               i = the_Intg i'; 
-               n = Inr i;
-        (T,k,cs) = the_Arr (globs (store s) oref); 
-               f = (\<lambda>v (x,s). (raise_if (\<not>G,s\<turnstile>v fits T) 
+definition
+  avar :: "prog \<Rightarrow> val \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state" where
+  "avar G i' a' s =
+    (let   oref = Heap (the_Addr a'); 
+              i = the_Intg i'; 
+              n = Inr i;
+       (T,k,cs) = the_Arr (globs (store s) oref); 
+              f = (\<lambda>v (x,s). (raise_if (\<not>G,s\<turnstile>v fits T) 
                                            ArrStore x
                               ,upd_gobj oref n v s)) 
-      in ((the (cs n),f)
-         ,abupd (raise_if (\<not>i in_bounds k) IndOutBound \<circ> np a') s)"
+     in ((the (cs n),f),abupd (raise_if (\<not>i in_bounds k) IndOutBound \<circ> np a') s))"
 
 lemma fvar_def2: --{* better suited for simplification *} 
 "fvar C stat fn a' s =  
@@ -431,27 +443,29 @@
 apply (simp (no_asm) add: Let_def split_beta)
 done
 
-definition check_field_access :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> vname \<Rightarrow> bool \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" where
-"check_field_access G accC statDeclC fn stat a' s
- \<equiv> let oref = if stat then Stat statDeclC
-                      else Heap (the_Addr a');
-       dynC = case oref of
+definition
+  check_field_access :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> vname \<Rightarrow> bool \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" where
+  "check_field_access G accC statDeclC fn stat a' s =
+    (let oref = if stat then Stat statDeclC
+                else Heap (the_Addr a');
+         dynC = case oref of
                    Heap a \<Rightarrow> obj_class (the (globs (store s) oref))
                  | Stat C \<Rightarrow> C;
-       f    = (the (table_of (DeclConcepts.fields G dynC) (fn,statDeclC)))
-   in abupd 
+         f    = (the (table_of (DeclConcepts.fields G dynC) (fn,statDeclC)))
+     in abupd 
         (error_if (\<not> G\<turnstile>Field fn (statDeclC,f) in dynC dyn_accessible_from accC)
                   AccessViolation)
-        s"
+        s)"
 
-definition check_method_access :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> inv_mode \<Rightarrow>  sig \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" where
-"check_method_access G accC statT mode sig  a' s
- \<equiv> let invC = invocation_class mode (store s) a' statT;
+definition
+  check_method_access :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> inv_mode \<Rightarrow>  sig \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" where
+  "check_method_access G accC statT mode sig  a' s =
+    (let invC = invocation_class mode (store s) a' statT;
        dynM = the (dynlookup G statT invC sig)
-   in abupd 
+     in abupd 
         (error_if (\<not> G\<turnstile>Methd sig dynM in invC dyn_accessible_from accC)
                   AccessViolation)
-        s"
+        s)"
        
 section "evaluation judgments"
 
diff -r d9549f9da779 -r a79abb22ca9c src/HOL/Bali/Example.thy
--- a/src/HOL/Bali/Example.thy	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/Example.thy	Mon Jul 26 18:25:19 2010 +0200
@@ -70,22 +70,21 @@
 datatype vnam'  = arr' | vee' | z' | e'
 datatype label' = lab1'
 
-consts
-
-  tnam' :: "tnam'  \<Rightarrow> tnam"
-  vnam' :: "vnam'  \<Rightarrow> vname"
+axiomatization
+  tnam' :: "tnam'  \<Rightarrow> tnam" and
+  vnam' :: "vnam'  \<Rightarrow> vname" and
   label':: "label' \<Rightarrow> label"
-axioms  (** tnam', vnam' and label are intended to be isomorphic 
+where
+  (** tnam', vnam' and label are intended to be isomorphic 
             to tnam, vname and label **)
 
-  inj_tnam'  [simp]: "(tnam'  x = tnam'  y) = (x = y)"
-  inj_vnam'  [simp]: "(vnam'  x = vnam'  y) = (x = y)"
-  inj_label' [simp]: "(label' x = label' y) = (x = y)"
-  
-  
-  surj_tnam':  "\<exists>m. n = tnam'  m"
-  surj_vnam':  "\<exists>m. n = vnam'  m"
-  surj_label':" \<exists>m. n = label' m"
+  inj_tnam'  [simp]: "\<And>x y. (tnam'  x = tnam'  y) = (x = y)" and
+  inj_vnam'  [simp]: "\<And>x y. (vnam'  x = vnam'  y) = (x = y)" and
+  inj_label' [simp]: "\<And>x y. (label' x = label' y) = (x = y)" and
+    
+  surj_tnam':  "\<And>n. \<exists>m. n = tnam'  m" and
+  surj_vnam':  "\<And>n. \<exists>m. n = vnam'  m" and
+  surj_label':" \<And>n. \<exists>m. n = label' m"
 
 abbreviation
   HasFoo :: qtname where
@@ -149,22 +148,24 @@
   Object_mdecls_def: "Object_mdecls \<equiv> []"
   SXcpt_mdecls_def:  "SXcpt_mdecls  \<equiv> []"
 
-consts
-  
+axiomatization  
   foo    :: mname
 
-definition foo_sig :: sig
- where "foo_sig   \<equiv> \<lparr>name=foo,parTs=[Class Base]\<rparr>"
+definition
+  foo_sig :: sig
+  where "foo_sig = \<lparr>name=foo,parTs=[Class Base]\<rparr>"
   
-definition foo_mhead :: mhead
- where "foo_mhead \<equiv> \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>"
+definition
+  foo_mhead :: mhead
+  where "foo_mhead = \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>"
 
-definition Base_foo :: mdecl
- where "Base_foo \<equiv> (foo_sig, \<lparr>access=Public,static=False,pars=[z],resT=Class Base,
+definition
+  Base_foo :: mdecl
+  where "Base_foo = (foo_sig, \<lparr>access=Public,static=False,pars=[z],resT=Class Base,
                         mbody=\<lparr>lcls=[],stmt=Return (!!z)\<rparr>\<rparr>)"
 
 definition Ext_foo :: mdecl
- where "Ext_foo  \<equiv> (foo_sig, 
+  where "Ext_foo = (foo_sig, 
               \<lparr>access=Public,static=False,pars=[z],resT=Class Ext,
                mbody=\<lparr>lcls=[]
                      ,stmt=Expr({Ext,Ext,False}Cast (Class Ext) (!!z)..vee := 
@@ -172,11 +173,13 @@
                                 Return (Lit Null)\<rparr>
               \<rparr>)"
 
-definition arr_viewed_from :: "qtname \<Rightarrow> qtname \<Rightarrow> var" where
-"arr_viewed_from accC C \<equiv> {accC,Base,True}StatRef (ClassT C)..arr"
+definition
+  arr_viewed_from :: "qtname \<Rightarrow> qtname \<Rightarrow> var"
+  where "arr_viewed_from accC C = {accC,Base,True}StatRef (ClassT C)..arr"
 
-definition BaseCl :: "class" where
-"BaseCl \<equiv> \<lparr>access=Public,
+definition
+  BaseCl :: "class" where
+  "BaseCl = \<lparr>access=Public,
            cfields=[(arr, \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>),
                     (vee, \<lparr>access=Public,static=False,type=Iface HasFoo    \<rparr>)],
            methods=[Base_foo],
@@ -185,16 +188,18 @@
            super=Object,
            superIfs=[HasFoo]\<rparr>"
   
-definition ExtCl  :: "class" where
-"ExtCl  \<equiv> \<lparr>access=Public,
+definition
+  ExtCl  :: "class" where
+  "ExtCl = \<lparr>access=Public,
            cfields=[(vee, \<lparr>access=Public,static=False,type= PrimT Integer\<rparr>)], 
            methods=[Ext_foo],
            init=Skip,
            super=Base,
            superIfs=[]\<rparr>"
 
-definition MainCl :: "class" where
-"MainCl \<equiv> \<lparr>access=Public,
+definition
+  MainCl :: "class" where
+  "MainCl = \<lparr>access=Public,
            cfields=[], 
            methods=[], 
            init=Skip,
@@ -202,14 +207,17 @@
            superIfs=[]\<rparr>"
 (* The "main" method is modeled seperately (see tprg) *)
 
-definition HasFooInt :: iface
- where "HasFooInt \<equiv> \<lparr>access=Public,imethods=[(foo_sig, foo_mhead)],isuperIfs=[]\<rparr>"
+definition
+  HasFooInt :: iface
+  where "HasFooInt = \<lparr>access=Public,imethods=[(foo_sig, foo_mhead)],isuperIfs=[]\<rparr>"
 
-definition Ifaces ::"idecl list"
- where "Ifaces \<equiv> [(HasFoo,HasFooInt)]"
+definition
+  Ifaces ::"idecl list"
+  where "Ifaces = [(HasFoo,HasFooInt)]"
 
-definition "Classes" ::"cdecl list"
- where "Classes \<equiv> [(Base,BaseCl),(Ext,ExtCl),(Main,MainCl)]@standard_classes"
+definition
+  "Classes" ::"cdecl list"
+  where "Classes = [(Base,BaseCl),(Ext,ExtCl),(Main,MainCl)]@standard_classes"
 
 lemmas table_classes_defs = 
      Classes_def standard_classes_def ObjectC_def SXcptC_def
@@ -264,12 +272,13 @@
   tprg :: prog where
   "tprg == \<lparr>ifaces=Ifaces,classes=Classes\<rparr>"
 
-definition test :: "(ty)list \<Rightarrow> stmt" where
- "test pTs \<equiv> e:==NewC Ext;; 
+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)
            (lab1\<bullet> While(Acc 
-                        (Acc (arr_viewed_from Main Ext).[Lit (Intg 2)])) Skip)"
+                        (Acc (arr_viewed_from Main Ext).[Lit (Intg 2)])) Skip))"
 
 
 section "well-structuredness"
@@ -1185,9 +1194,9 @@
          rewrite_rule [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *}
 lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros
 
-consts
-  a :: loc
-  b :: loc
+axiomatization
+  a :: loc and
+  b :: loc and
   c :: loc
 
 abbreviation "one == Suc 0"
diff -r d9549f9da779 -r a79abb22ca9c src/HOL/Bali/Name.thy
--- a/src/HOL/Bali/Name.thy	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/Name.thy	Mon Jul 26 18:25:19 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
diff -r d9549f9da779 -r a79abb22ca9c src/HOL/Bali/State.thy
--- a/src/HOL/Bali/State.thy	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/State.thy	Mon Jul 26 18:25:19 2010 +0200
@@ -38,8 +38,9 @@
   (type) "obj"   <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option\<rparr>"
   (type) "obj"   <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option,\<dots>::'a\<rparr>"
 
-definition the_Arr :: "obj option \<Rightarrow> ty \<times> int \<times> (vn, val) table" where
- "the_Arr obj \<equiv> SOME (T,k,t). obj = Some \<lparr>tag=Arr T k,values=t\<rparr>"
+definition
+  the_Arr :: "obj option \<Rightarrow> ty \<times> int \<times> (vn, val) table"
+  where "the_Arr obj = (SOME (T,k,t). obj = Some \<lparr>tag=Arr T k,values=t\<rparr>)"
 
 lemma the_Arr_Arr [simp]: "the_Arr (Some \<lparr>tag=Arr T k,values=cs\<rparr>) = (T,k,cs)"
 apply (auto simp: the_Arr_def)
@@ -50,18 +51,20 @@
 apply (auto simp add: the_Arr_def)
 done
 
-definition upd_obj :: "vn \<Rightarrow> val \<Rightarrow> obj \<Rightarrow> obj" where 
- "upd_obj n v \<equiv> \<lambda> obj . obj \<lparr>values:=(values obj)(n\<mapsto>v)\<rparr>"
+definition
+  upd_obj :: "vn \<Rightarrow> val \<Rightarrow> obj \<Rightarrow> obj"
+  where "upd_obj n v = (\<lambda>obj. obj \<lparr>values:=(values obj)(n\<mapsto>v)\<rparr>)"
 
 lemma upd_obj_def2 [simp]: 
   "upd_obj n v obj = obj \<lparr>values:=(values obj)(n\<mapsto>v)\<rparr>" 
 apply (auto simp: upd_obj_def)
 done
 
-definition obj_ty :: "obj \<Rightarrow> ty" where
- "obj_ty obj    \<equiv> case tag obj of 
-                    CInst C \<Rightarrow> Class C 
-                  | Arr T k \<Rightarrow> T.[]"
+definition
+  obj_ty :: "obj \<Rightarrow> ty" where
+  "obj_ty obj = (case tag obj of 
+                  CInst C \<Rightarrow> Class C 
+                | Arr T k \<Rightarrow> T.[])"
 
 lemma obj_ty_eq [intro!]: "obj_ty \<lparr>tag=oi,values=x\<rparr> = obj_ty \<lparr>tag=oi,values=y\<rparr>" 
 by (simp add: obj_ty_def)
@@ -97,10 +100,11 @@
 apply (auto split add: obj_tag.split_asm)
 done
 
-definition obj_class :: "obj \<Rightarrow> qtname" where
- "obj_class obj \<equiv> case tag obj of 
-                    CInst C \<Rightarrow> C 
-                  | Arr T k \<Rightarrow> Object"
+definition
+  obj_class :: "obj \<Rightarrow> qtname" where
+  "obj_class obj = (case tag obj of 
+                     CInst C \<Rightarrow> C 
+                   | Arr T k \<Rightarrow> Object)"
 
 
 lemma obj_class_CInst [simp]: "obj_class \<lparr>tag=CInst C,values=vs\<rparr> = C" 
@@ -136,9 +140,10 @@
   "Stat" => "CONST Inr"
   (type) "oref" <= (type) "loc + qtname"
 
-definition fields_table :: "prog \<Rightarrow> qtname \<Rightarrow> (fspec \<Rightarrow> field \<Rightarrow> bool)  \<Rightarrow> (fspec, ty) table" where
- "fields_table G C P 
-    \<equiv> Option.map type \<circ> table_of (filter (split P) (DeclConcepts.fields G C))"
+definition
+  fields_table :: "prog \<Rightarrow> qtname \<Rightarrow> (fspec \<Rightarrow> field \<Rightarrow> bool)  \<Rightarrow> (fspec, ty) table" where
+  "fields_table G C P =
+    Option.map type \<circ> table_of (filter (split P) (DeclConcepts.fields G C))"
 
 lemma fields_table_SomeI: 
 "\<lbrakk>table_of (DeclConcepts.fields G C) n = Some f; P n f\<rbrakk> 
@@ -173,20 +178,23 @@
 apply simp
 done
 
-definition in_bounds :: "int \<Rightarrow> int \<Rightarrow> bool" ("(_/ in'_bounds _)" [50, 51] 50) where
- "i in_bounds k \<equiv> 0 \<le> i \<and> i < k"
+definition
+  in_bounds :: "int \<Rightarrow> int \<Rightarrow> bool" ("(_/ in'_bounds _)" [50, 51] 50)
+  where "i in_bounds k = (0 \<le> i \<and> i < k)"
 
-definition arr_comps :: "'a \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a option" where
- "arr_comps T k \<equiv> \<lambda>i. if i in_bounds k then Some T else None"
+definition
+  arr_comps :: "'a \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a option"
+  where "arr_comps T k = (\<lambda>i. if i in_bounds k then Some T else None)"
   
-definition var_tys       :: "prog \<Rightarrow> obj_tag \<Rightarrow> oref \<Rightarrow> (vn, ty) table" where
-"var_tys G oi r 
-  \<equiv> case r of 
+definition
+  var_tys :: "prog \<Rightarrow> obj_tag \<Rightarrow> oref \<Rightarrow> (vn, ty) table" where
+  "var_tys G oi r =
+    (case r of 
       Heap a \<Rightarrow> (case oi of 
                    CInst C \<Rightarrow> fields_table G C (\<lambda>n f. \<not>static f) (+) empty
                  | Arr T k \<Rightarrow> empty (+) arr_comps T k)
     | Stat C \<Rightarrow> fields_table G C (\<lambda>fn f. declclassf fn = C \<and> static f) 
-                (+) empty"
+                (+) empty)"
 
 lemma var_tys_Some_eq: 
  "var_tys G oi r n = Some T 
@@ -222,14 +230,16 @@
 
 subsection "access"
 
-definition globs :: "st \<Rightarrow> globs" where
- "globs  \<equiv> st_case (\<lambda>g l. g)"
+definition
+  globs :: "st \<Rightarrow> globs"
+  where "globs = st_case (\<lambda>g l. g)"
   
-definition locals :: "st \<Rightarrow> locals" where
- "locals \<equiv> st_case (\<lambda>g l. l)"
+definition
+  locals :: "st \<Rightarrow> locals"
+  where "locals = st_case (\<lambda>g l. l)"
 
-definition heap   :: "st \<Rightarrow> heap" where
- "heap s \<equiv> globs s \<circ> Heap"
+definition heap :: "st \<Rightarrow> heap" where
+ "heap s = globs s \<circ> Heap"
 
 
 lemma globs_def2 [simp]: " globs (st g l) = g"
@@ -250,8 +260,9 @@
 
 subsection "memory allocation"
 
-definition new_Addr :: "heap \<Rightarrow> loc option" where
- "new_Addr h   \<equiv> if (\<forall>a. h a \<noteq> None) then None else Some (SOME a. h a = None)"
+definition
+  new_Addr :: "heap \<Rightarrow> loc option" where
+  "new_Addr h = (if (\<forall>a. h a \<noteq> None) then None else Some (SOME a. h a = None))"
 
 lemma new_AddrD: "new_Addr h = Some a \<Longrightarrow> h a = None"
 apply (auto simp add: new_Addr_def)
@@ -290,20 +301,25 @@
 
 subsection "update"
 
-definition gupd :: "oref  \<Rightarrow> obj \<Rightarrow> st \<Rightarrow> st" ("gupd'(_\<mapsto>_')"[10,10]1000) where
- "gupd r obj  \<equiv> st_case (\<lambda>g l. st (g(r\<mapsto>obj)) l)"
+definition
+  gupd :: "oref  \<Rightarrow> obj \<Rightarrow> st \<Rightarrow> st" ("gupd'(_\<mapsto>_')" [10, 10] 1000)
+  where "gupd r obj = st_case (\<lambda>g l. st (g(r\<mapsto>obj)) l)"
 
-definition lupd       :: "lname \<Rightarrow> val \<Rightarrow> st \<Rightarrow> st" ("lupd'(_\<mapsto>_')"[10,10]1000) where
- "lupd vn v   \<equiv> st_case (\<lambda>g l. st g (l(vn\<mapsto>v)))"
+definition
+  lupd :: "lname \<Rightarrow> val \<Rightarrow> st \<Rightarrow> st" ("lupd'(_\<mapsto>_')" [10, 10] 1000)
+  where "lupd vn v = st_case (\<lambda>g l. st g (l(vn\<mapsto>v)))"
 
-definition upd_gobj   :: "oref \<Rightarrow> vn \<Rightarrow> val \<Rightarrow> st \<Rightarrow> st" where
- "upd_gobj r n v \<equiv> st_case (\<lambda>g l. st (chg_map (upd_obj n v) r g) l)"
+definition
+  upd_gobj :: "oref \<Rightarrow> vn \<Rightarrow> val \<Rightarrow> st \<Rightarrow> st"
+  where "upd_gobj r n v = st_case (\<lambda>g l. st (chg_map (upd_obj n v) r g) l)"
 
-definition set_locals  :: "locals \<Rightarrow> st \<Rightarrow> st" where
- "set_locals l \<equiv> st_case (\<lambda>g l'. st g l)"
+definition
+  set_locals  :: "locals \<Rightarrow> st \<Rightarrow> st"
+  where "set_locals l = st_case (\<lambda>g l'. st g l)"
 
-definition init_obj    :: "prog \<Rightarrow> obj_tag \<Rightarrow> oref \<Rightarrow> st \<Rightarrow> st" where
- "init_obj G oi r \<equiv> gupd(r\<mapsto>\<lparr>tag=oi, values=init_vals (var_tys G oi r)\<rparr>)"
+definition
+  init_obj :: "prog \<Rightarrow> obj_tag \<Rightarrow> oref \<Rightarrow> st \<Rightarrow> st"
+  where "init_obj G oi r = gupd(r\<mapsto>\<lparr>tag=oi, values=init_vals (var_tys G oi r)\<rparr>)"
 
 abbreviation
   init_class_obj :: "prog \<Rightarrow> qtname \<Rightarrow> st \<Rightarrow> st"
@@ -447,23 +463,22 @@
 
 
 
-consts
+primrec the_Xcpt :: "abrupt \<Rightarrow> xcpt"
+  where "the_Xcpt (Xcpt x) = x"
 
-  the_Xcpt :: "abrupt \<Rightarrow> xcpt"
-  the_Jump :: "abrupt => jump"
-  the_Loc  :: "xcpt \<Rightarrow> loc"
-  the_Std  :: "xcpt \<Rightarrow> xname"
+primrec the_Jump :: "abrupt => jump"
+  where "the_Jump (Jump j) = j"
 
-primrec "the_Xcpt (Xcpt x) = x"
-primrec "the_Jump (Jump j) = j"
-primrec "the_Loc (Loc a) = a"
-primrec "the_Std (Std x) = x"
+primrec the_Loc :: "xcpt \<Rightarrow> loc"
+  where "the_Loc (Loc a) = a"
 
-
+primrec the_Std :: "xcpt \<Rightarrow> xname"
+  where "the_Std (Std x) = x"
         
 
-definition abrupt_if :: "bool \<Rightarrow> abopt \<Rightarrow> abopt \<Rightarrow> abopt" where
- "abrupt_if c x' x \<equiv> if c \<and> (x = None) then x' else x"
+definition
+  abrupt_if :: "bool \<Rightarrow> abopt \<Rightarrow> abopt \<Rightarrow> abopt"
+  where "abrupt_if c x' x = (if c \<and> (x = None) then x' else x)"
 
 lemma abrupt_if_True_None [simp]: "abrupt_if True x None = x"
 by (simp add: abrupt_if_def)
@@ -542,8 +557,9 @@
 apply auto
 done
 
-definition absorb :: "jump \<Rightarrow> abopt \<Rightarrow> abopt" where
-  "absorb j a \<equiv> if a=Some (Jump j) then None else a"
+definition
+  absorb :: "jump \<Rightarrow> abopt \<Rightarrow> abopt"
+  where "absorb j a = (if a=Some (Jump j) then None else a)"
 
 lemma absorb_SomeD [dest!]: "absorb j a = Some x \<Longrightarrow> a = Some x"
 by (auto simp add: absorb_def)
@@ -593,16 +609,18 @@
 apply clarsimp
 done
 
-definition normal :: "state \<Rightarrow> bool" where
- "normal \<equiv> \<lambda>s. abrupt s = None"
+definition
+  normal :: "state \<Rightarrow> bool"
+  where "normal = (\<lambda>s. abrupt s = None)"
 
 lemma normal_def2 [simp]: "normal s = (abrupt s = None)"
 apply (unfold normal_def)
 apply (simp (no_asm))
 done
 
-definition heap_free :: "nat \<Rightarrow> state \<Rightarrow> bool" where
- "heap_free n \<equiv> \<lambda>s. atleast_free (heap (store s)) n"
+definition
+  heap_free :: "nat \<Rightarrow> state \<Rightarrow> bool"
+  where "heap_free n = (\<lambda>s. atleast_free (heap (store s)) n)"
 
 lemma heap_free_def2 [simp]: "heap_free n s = atleast_free (heap (store s)) n"
 apply (unfold heap_free_def)
@@ -611,11 +629,13 @@
 
 subsection "update"
 
-definition abupd :: "(abopt \<Rightarrow> abopt) \<Rightarrow> state \<Rightarrow> state" where
- "abupd f \<equiv> prod_fun f id"
+definition
+  abupd :: "(abopt \<Rightarrow> abopt) \<Rightarrow> state \<Rightarrow> state"
+  where "abupd f = prod_fun f id"
 
-definition supd     :: "(st \<Rightarrow> st) \<Rightarrow> state \<Rightarrow> state" where
- "supd \<equiv> prod_fun id"
+definition
+  supd :: "(st \<Rightarrow> st) \<Rightarrow> state \<Rightarrow> state"
+  where "supd = prod_fun id"
   
 lemma abupd_def2 [simp]: "abupd f (x,s) = (f x,s)"
 by (simp add: abupd_def)
@@ -669,11 +689,13 @@
 
 section "initialisation test"
 
-definition inited :: "qtname \<Rightarrow> globs \<Rightarrow> bool" where
- "inited C g \<equiv> g (Stat C) \<noteq> None"
+definition
+  inited :: "qtname \<Rightarrow> globs \<Rightarrow> bool"
+  where "inited C g = (g (Stat C) \<noteq> None)"
 
-definition initd    :: "qtname \<Rightarrow> state \<Rightarrow> bool" where
- "initd C \<equiv> inited C \<circ> globs \<circ> store"
+definition
+  initd :: "qtname \<Rightarrow> state \<Rightarrow> bool"
+  where "initd C = inited C \<circ> globs \<circ> store"
 
 lemma not_inited_empty [simp]: "\<not>inited C empty"
 apply (unfold inited_def)
@@ -706,8 +728,10 @@
 done
 
 section {* @{text error_free} *}
-definition error_free :: "state \<Rightarrow> bool" where
-"error_free s \<equiv> \<not> (\<exists> err. abrupt s = Some (Error err))"
+
+definition
+  error_free :: "state \<Rightarrow> bool"
+  where "error_free s = (\<not> (\<exists> err. abrupt s = Some (Error err)))"
 
 lemma error_free_Norm [simp,intro]: "error_free (Norm s)"
 by (simp add: error_free_def)
diff -r d9549f9da779 -r a79abb22ca9c src/HOL/Bali/Table.thy
--- a/src/HOL/Bali/Table.thy	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/Table.thy	Mon Jul 26 18:25:19 2010 +0200
@@ -54,15 +54,15 @@
 
 --{* when merging tables old and new, only override an entry of table old when  
    the condition cond holds *}
-"cond_override cond old new \<equiv>
- \<lambda> k.
+"cond_override cond old new =
+ (\<lambda>k.
   (case new k of
      None         \<Rightarrow> old k                       
    | Some new_val \<Rightarrow> (case old k of
                         None         \<Rightarrow> Some new_val          
                       | Some old_val \<Rightarrow> (if cond new_val old_val
                                          then Some new_val     
-                                         else Some old_val)))"
+                                         else Some old_val))))"
 
 lemma cond_override_empty1[simp]: "cond_override c empty t = t"
 by (simp add: cond_override_def expand_fun_eq)
@@ -95,10 +95,11 @@
 
 section {* Filter on Tables *}
 
-definition filter_tab :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" where
-"filter_tab c t \<equiv> \<lambda> k. (case t k of 
+definition
+  filter_tab :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" where
+  "filter_tab c t = (\<lambda>k. (case t k of 
                            None   \<Rightarrow> None
-                         | Some x \<Rightarrow> if c k x then Some x else None)"
+                         | Some x \<Rightarrow> if c k x then Some x else None))"
 
 lemma filter_tab_empty[simp]: "filter_tab c empty = empty"
 by (simp add: filter_tab_def empty_def)
@@ -279,27 +280,31 @@
 done
 
 
-consts
-  Un_tables      :: "('a, 'b) tables set \<Rightarrow> ('a, 'b) tables"
-  overrides_t    :: "('a, 'b) tables     \<Rightarrow> ('a, 'b) tables \<Rightarrow>
-                     ('a, 'b) tables"             (infixl "\<oplus>\<oplus>" 100)
-  hidings_entails:: "('a, 'b) tables \<Rightarrow> ('a, 'c) tables \<Rightarrow> 
-                     ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool"   ("_ hidings _ entails _" 20)
+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
+  overrides_t :: "('a, 'b) tables \<Rightarrow> ('a, 'b) tables \<Rightarrow> ('a, 'b) tables"  (infixl "\<oplus>\<oplus>" 100)
+  where "s \<oplus>\<oplus> t = (\<lambda>k. if t k = {} then s k else t k)"
+
+definition
+  hidings_entails :: "('a, 'b) tables \<Rightarrow> ('a, 'c) tables \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool"
+    ("_ hidings _ entails _" 20)
+  where "(t hidings s entails R) = (\<forall>k. \<forall>x\<in>t k. \<forall>y\<in>s k. R x y)"
+
+definition
   --{* variant for unique table: *}
-  hiding_entails :: "('a, 'b) table  \<Rightarrow> ('a, 'c) table  \<Rightarrow> 
-                     ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool"   ("_ hiding _ entails _"  20)
+  hiding_entails :: "('a, 'b) table  \<Rightarrow> ('a, 'c) table  \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool"
+    ("_ hiding _ entails _"  20)
+  where "(t hiding  s entails R) = (\<forall>k. \<forall>x\<in>t k: \<forall>y\<in>s k: R x y)"
+
+definition
   --{* variant for a unique table and conditional overriding: *}
   cond_hiding_entails :: "('a, 'b) table  \<Rightarrow> ('a, 'c) table  
                           \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool"  
                           ("_ hiding _ under _ entails _"  20)
-
-defs
-  Un_tables_def:       "Un_tables ts\<spacespace>\<spacespace>\<equiv> \<lambda>k. \<Union>t\<in>ts. t k"
-  overrides_t_def:     "s \<oplus>\<oplus> t        \<equiv> \<lambda>k. if t k = {} then s k else t k"
-  hidings_entails_def: "t hidings s entails R \<equiv> \<forall>k. \<forall>x\<in>t k. \<forall>y\<in>s k. R x y"
-  hiding_entails_def:  "t hiding  s entails R \<equiv> \<forall>k. \<forall>x\<in>t k: \<forall>y\<in>s k: R x y"
-  cond_hiding_entails_def: "t hiding  s under C entails R
-                            \<equiv> \<forall>k. \<forall>x\<in>t k: \<forall>y\<in>s k: C x y \<longrightarrow> R x y"
+  where "(t hiding  s under C entails R) = (\<forall>k. \<forall>x\<in>t k: \<forall>y\<in>s k: C x y \<longrightarrow> R x y)"
 
 section "Untables"
 
@@ -383,12 +388,10 @@
 
 
 (*###TO Map?*)
-consts
-  atleast_free :: "('a ~=> 'b) => nat => bool"
-primrec
- "atleast_free m 0       = True"
- atleast_free_Suc: 
- "atleast_free m (Suc n) = (? a. m a = None & (!b. atleast_free (m(a|->b)) n))"
+primrec atleast_free :: "('a ~=> 'b) => nat => bool"
+where
+  "atleast_free m 0 = True"
+| atleast_free_Suc: "atleast_free m (Suc n) = (\<exists>a. m a = None & (!b. atleast_free (m(a|->b)) n))"
 
 lemma atleast_free_weaken [rule_format (no_asm)]: 
   "!m. atleast_free m (Suc n) \<longrightarrow> atleast_free m n"
diff -r d9549f9da779 -r a79abb22ca9c src/HOL/Bali/Term.thy
--- a/src/HOL/Bali/Term.thy	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/Term.thy	Mon Jul 26 18:25:19 2010 +0200
@@ -258,8 +258,9 @@
   StatRef :: "ref_ty \<Rightarrow> expr"
   where "StatRef rt == Cast (RefT rt) (Lit Null)"
   
-definition is_stmt :: "term \<Rightarrow> bool" where
- "is_stmt t \<equiv> \<exists>c. t=In1r c"
+definition
+  is_stmt :: "term \<Rightarrow> bool"
+  where "is_stmt t = (\<exists>c. t=In1r c)"
 
 ML {* bind_thms ("is_stmt_rews", sum3_instantiate @{context} @{thm is_stmt_def}) *}
 
@@ -307,7 +308,7 @@
 begin
 
 definition
-  stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c"
+  stmt_inj_term_def: "\<langle>c::stmt\<rangle> = In1r c"
 
 instance ..
 
@@ -323,7 +324,7 @@
 begin
 
 definition
-  expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e"
+  expr_inj_term_def: "\<langle>e::expr\<rangle> = In1l e"
 
 instance ..
 
@@ -339,7 +340,7 @@
 begin
 
 definition
-  var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v"
+  var_inj_term_def: "\<langle>v::var\<rangle> = In2 v"
 
 instance ..
 
@@ -368,7 +369,7 @@
 begin
 
 definition
-  "\<langle>es::'a list\<rangle> \<equiv> In3 (map expr_of es)"
+  "\<langle>es::'a list\<rangle> = In3 (map expr_of es)"
 
 instance ..
 
@@ -425,46 +426,47 @@
   done
 
 section {* Evaluation of unary operations *}
-consts eval_unop :: "unop \<Rightarrow> val \<Rightarrow> val"
-primrec
-"eval_unop UPlus   v = Intg (the_Intg v)"
-"eval_unop UMinus  v = Intg (- (the_Intg v))"
-"eval_unop UBitNot v = Intg 42"                -- "FIXME: Not yet implemented"
-"eval_unop UNot    v = Bool (\<not> the_Bool v)"
+primrec eval_unop :: "unop \<Rightarrow> val \<Rightarrow> val"
+where
+  "eval_unop UPlus v = Intg (the_Intg v)"
+| "eval_unop UMinus v = Intg (- (the_Intg v))"
+| "eval_unop UBitNot v = Intg 42"                -- "FIXME: Not yet implemented"
+| "eval_unop UNot v = Bool (\<not> the_Bool v)"
 
 section {* Evaluation of binary operations *}
-consts eval_binop :: "binop \<Rightarrow> val \<Rightarrow> val \<Rightarrow> val"
-primrec
-"eval_binop Mul     v1 v2 = Intg ((the_Intg v1) * (the_Intg v2))" 
-"eval_binop Div     v1 v2 = Intg ((the_Intg v1) div (the_Intg v2))"
-"eval_binop Mod     v1 v2 = Intg ((the_Intg v1) mod (the_Intg v2))"
-"eval_binop Plus    v1 v2 = Intg ((the_Intg v1) + (the_Intg v2))"
-"eval_binop Minus   v1 v2 = Intg ((the_Intg v1) - (the_Intg v2))"
+primrec eval_binop :: "binop \<Rightarrow> val \<Rightarrow> val \<Rightarrow> val"
+where
+  "eval_binop Mul     v1 v2 = Intg ((the_Intg v1) * (the_Intg v2))" 
+| "eval_binop Div     v1 v2 = Intg ((the_Intg v1) div (the_Intg v2))"
+| "eval_binop Mod     v1 v2 = Intg ((the_Intg v1) mod (the_Intg v2))"
+| "eval_binop Plus    v1 v2 = Intg ((the_Intg v1) + (the_Intg v2))"
+| "eval_binop Minus   v1 v2 = Intg ((the_Intg v1) - (the_Intg v2))"
 
 -- "Be aware of the explicit coercion of the shift distance to nat"
-"eval_binop LShift  v1 v2 = Intg ((the_Intg v1) *   (2^(nat (the_Intg v2))))"
-"eval_binop RShift  v1 v2 = Intg ((the_Intg v1) div (2^(nat (the_Intg v2))))"
-"eval_binop RShiftU v1 v2 = Intg 42" --"FIXME: Not yet implemented"
+| "eval_binop LShift  v1 v2 = Intg ((the_Intg v1) *   (2^(nat (the_Intg v2))))"
+| "eval_binop RShift  v1 v2 = Intg ((the_Intg v1) div (2^(nat (the_Intg v2))))"
+| "eval_binop RShiftU v1 v2 = Intg 42" --"FIXME: Not yet implemented"
 
-"eval_binop Less    v1 v2 = Bool ((the_Intg v1) < (the_Intg v2))" 
-"eval_binop Le      v1 v2 = Bool ((the_Intg v1) \<le> (the_Intg v2))"
-"eval_binop Greater v1 v2 = Bool ((the_Intg v2) < (the_Intg v1))"
-"eval_binop Ge      v1 v2 = Bool ((the_Intg v2) \<le> (the_Intg v1))"
+| "eval_binop Less    v1 v2 = Bool ((the_Intg v1) < (the_Intg v2))" 
+| "eval_binop Le      v1 v2 = Bool ((the_Intg v1) \<le> (the_Intg v2))"
+| "eval_binop Greater v1 v2 = Bool ((the_Intg v2) < (the_Intg v1))"
+| "eval_binop Ge      v1 v2 = Bool ((the_Intg v2) \<le> (the_Intg v1))"
 
-"eval_binop Eq      v1 v2 = Bool (v1=v2)"
-"eval_binop Neq     v1 v2 = Bool (v1\<noteq>v2)"
-"eval_binop BitAnd  v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
-"eval_binop And     v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
-"eval_binop BitXor  v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
-"eval_binop Xor     v1 v2 = Bool ((the_Bool v1) \<noteq> (the_Bool v2))"
-"eval_binop BitOr   v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
-"eval_binop Or      v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
-"eval_binop CondAnd v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
-"eval_binop CondOr  v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
+| "eval_binop Eq      v1 v2 = Bool (v1=v2)"
+| "eval_binop Neq     v1 v2 = Bool (v1\<noteq>v2)"
+| "eval_binop BitAnd  v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
+| "eval_binop And     v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
+| "eval_binop BitXor  v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
+| "eval_binop Xor     v1 v2 = Bool ((the_Bool v1) \<noteq> (the_Bool v2))"
+| "eval_binop BitOr   v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
+| "eval_binop Or      v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
+| "eval_binop CondAnd v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
+| "eval_binop CondOr  v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
 
-definition need_second_arg :: "binop \<Rightarrow> val \<Rightarrow> bool" where
-"need_second_arg binop v1 \<equiv> \<not> ((binop=CondAnd \<and>  \<not> the_Bool v1) \<or>
-                               (binop=CondOr  \<and> the_Bool v1))"
+definition
+  need_second_arg :: "binop \<Rightarrow> val \<Rightarrow> bool" where
+  "need_second_arg binop v1 = (\<not> ((binop=CondAnd \<and>  \<not> the_Bool v1) \<or>
+                                 (binop=CondOr  \<and> the_Bool v1)))"
 text {* @{term CondAnd} and @{term CondOr} only evalulate the second argument
  if the value isn't already determined by the first argument*}
 
diff -r d9549f9da779 -r a79abb22ca9c src/HOL/Bali/Trans.thy
--- a/src/HOL/Bali/Trans.thy	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/Trans.thy	Mon Jul 26 18:25:19 2010 +0200
@@ -9,12 +9,13 @@
 
 theory Trans imports Evaln begin
 
-definition groundVar :: "var \<Rightarrow> bool" where
-"groundVar v \<longleftrightarrow> (case v of
-                   LVar ln \<Rightarrow> True
-                 | {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a
-                 | e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i
-                 | InsInitV c v \<Rightarrow> False)"
+definition
+  groundVar :: "var \<Rightarrow> bool" where
+  "groundVar v \<longleftrightarrow> (case v of
+                     LVar ln \<Rightarrow> True
+                   | {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a
+                   | e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i
+                   | InsInitV c v \<Rightarrow> False)"
 
 lemma groundVar_cases [consumes 1, case_names LVar FVar AVar]:
   assumes ground: "groundVar v" and
@@ -34,14 +35,15 @@
     done
 qed
 
-definition groundExprs :: "expr list \<Rightarrow> bool" where
-  "groundExprs es \<longleftrightarrow> (\<forall>e \<in> set es. \<exists>v. e = Lit v)"
+definition
+  groundExprs :: "expr list \<Rightarrow> bool"
+  where "groundExprs es \<longleftrightarrow> (\<forall>e \<in> set es. \<exists>v. e = Lit v)"
   
-primrec the_val:: "expr \<Rightarrow> val" where
-  "the_val (Lit v) = v"
+primrec the_val:: "expr \<Rightarrow> val"
+  where "the_val (Lit v) = v"
 
 primrec the_var:: "prog \<Rightarrow> state \<Rightarrow> var \<Rightarrow> (vvar \<times> state)" where
-  "the_var G s (LVar ln)                    =(lvar ln (store s),s)"
+  "the_var G s (LVar ln) = (lvar ln (store s),s)"
 | the_var_FVar_def: "the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s"
 | the_var_AVar_def: "the_var G s(a.[i])                       =avar G (the_val i) (the_val a) s"
 
diff -r d9549f9da779 -r a79abb22ca9c src/HOL/Bali/Type.thy
--- a/src/HOL/Bali/Type.thy	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/Type.thy	Mon Jul 26 18:25:19 2010 +0200
@@ -36,8 +36,9 @@
 abbreviation Array :: "ty \<Rightarrow> ty"  ("_.[]" [90] 90)
   where "T.[] == RefT (ArrayT T)"
 
-definition the_Class :: "ty \<Rightarrow> qtname" where
- "the_Class T \<equiv> SOME C. T = Class C" (** primrec not possible here **)
+definition
+  the_Class :: "ty \<Rightarrow> qtname"
+  where "the_Class T = (SOME C. T = Class C)" (** primrec not possible here **)
  
 lemma the_Class_eq [simp]: "the_Class (Class C)= C"
 by (auto simp add: the_Class_def)
diff -r d9549f9da779 -r a79abb22ca9c src/HOL/Bali/TypeRel.thy
--- a/src/HOL/Bali/TypeRel.thy	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/TypeRel.thy	Mon Jul 26 18:25:19 2010 +0200
@@ -25,14 +25,17 @@
 \end{itemize}
 *}
 
-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       *)
-  implmt1   :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct implementation *}
+
+definition
+  implmt1 :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct implementation *}
+  --{* direct implementation, cf. 8.1.3 *}
+  where "implmt1 G = {(C,I). C\<noteq>Object \<and> (\<exists>c\<in>class G C: I\<in>set (superIfs c))}"
+
 
 abbreviation
   subint1_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<:I1_" [71,71,71] 70)
@@ -325,16 +328,11 @@
 
 section "implementation relation"
 
-defs
-  --{* direct implementation, cf. 8.1.3 *}
-implmt1_def:"implmt1 G\<equiv>{(C,I). C\<noteq>Object \<and> (\<exists>c\<in>class G C: I\<in>set (superIfs c))}"
-
 lemma implmt1D: "G\<turnstile>C\<leadsto>1I \<Longrightarrow> C\<noteq>Object \<and> (\<exists>c\<in>class G C: I\<in>set (superIfs c))"
 apply (unfold implmt1_def)
 apply auto
 done
 
-
 inductive --{* implementation, cf. 8.1.4 *}
   implmt :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile>_\<leadsto>_" [71,71,71] 70)
   for G :: prog
@@ -568,8 +566,9 @@
 apply (fast dest: widen_Class_Class widen_Class_Iface)
 done
 
-definition widens :: "prog \<Rightarrow> [ty list, ty list] \<Rightarrow> bool" ("_\<turnstile>_[\<preceq>]_" [71,71,71] 70) where
- "G\<turnstile>Ts[\<preceq>]Ts' \<equiv> list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') Ts Ts'"
+definition
+  widens :: "prog \<Rightarrow> [ty list, ty list] \<Rightarrow> bool" ("_\<turnstile>_[\<preceq>]_" [71,71,71] 70)
+  where "G\<turnstile>Ts[\<preceq>]Ts' = list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') Ts Ts'"
 
 lemma widens_Nil [simp]: "G\<turnstile>[][\<preceq>][]"
 apply (unfold widens_def)
diff -r d9549f9da779 -r a79abb22ca9c src/HOL/Bali/TypeSafe.thy
--- a/src/HOL/Bali/TypeSafe.thy	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/TypeSafe.thy	Mon Jul 26 18:25:19 2010 +0200
@@ -93,23 +93,27 @@
 
 section "result conformance"
 
-definition assign_conforms :: "st \<Rightarrow> (val \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> ty \<Rightarrow> env' \<Rightarrow> bool" ("_\<le>|_\<preceq>_\<Colon>\<preceq>_" [71,71,71,71] 70) where
-"s\<le>|f\<preceq>T\<Colon>\<preceq>E \<equiv>
- (\<forall>s' w. Norm s'\<Colon>\<preceq>E \<longrightarrow> fst E,s'\<turnstile>w\<Colon>\<preceq>T \<longrightarrow> s\<le>|s' \<longrightarrow> assign f w (Norm s')\<Colon>\<preceq>E) \<and>
- (\<forall>s' w. error_free s' \<longrightarrow> (error_free (assign f w s')))"      
+definition
+  assign_conforms :: "st \<Rightarrow> (val \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> ty \<Rightarrow> env' \<Rightarrow> bool" ("_\<le>|_\<preceq>_\<Colon>\<preceq>_" [71,71,71,71] 70)
+where
+  "s\<le>|f\<preceq>T\<Colon>\<preceq>E =
+   ((\<forall>s' w. Norm s'\<Colon>\<preceq>E \<longrightarrow> fst E,s'\<turnstile>w\<Colon>\<preceq>T \<longrightarrow> s\<le>|s' \<longrightarrow> assign f w (Norm s')\<Colon>\<preceq>E) \<and>
+    (\<forall>s' w. error_free s' \<longrightarrow> (error_free (assign f w s'))))"
 
 
-definition rconf :: "prog \<Rightarrow> lenv \<Rightarrow> st \<Rightarrow> term \<Rightarrow> vals \<Rightarrow> tys \<Rightarrow> bool" ("_,_,_\<turnstile>_\<succ>_\<Colon>\<preceq>_" [71,71,71,71,71,71] 70) where
-  "G,L,s\<turnstile>t\<succ>v\<Colon>\<preceq>T 
-    \<equiv> case T of
-        Inl T  \<Rightarrow> if (\<exists> var. t=In2 var)
-                  then (\<forall> n. (the_In2 t) = LVar n 
-                         \<longrightarrow> (fst (the_In2 v) = the (locals s n)) \<and>
-                             (locals s n \<noteq> None \<longrightarrow> G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T)) \<and>
-                      (\<not> (\<exists> n. the_In2 t=LVar n) \<longrightarrow> (G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T))\<and>
-                      (s\<le>|snd (the_In2 v)\<preceq>T\<Colon>\<preceq>(G,L))
-                  else G,s\<turnstile>the_In1 v\<Colon>\<preceq>T
-      | Inr Ts \<Rightarrow> list_all2 (conf G s) (the_In3 v) Ts"
+definition
+  rconf :: "prog \<Rightarrow> lenv \<Rightarrow> st \<Rightarrow> term \<Rightarrow> vals \<Rightarrow> tys \<Rightarrow> bool" ("_,_,_\<turnstile>_\<succ>_\<Colon>\<preceq>_" [71,71,71,71,71,71] 70)
+where
+  "G,L,s\<turnstile>t\<succ>v\<Colon>\<preceq>T =
+    (case T of
+      Inl T  \<Rightarrow> if (\<exists> var. t=In2 var)
+                then (\<forall> n. (the_In2 t) = LVar n 
+                       \<longrightarrow> (fst (the_In2 v) = the (locals s n)) \<and>
+                           (locals s n \<noteq> None \<longrightarrow> G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T)) \<and>
+                    (\<not> (\<exists> n. the_In2 t=LVar n) \<longrightarrow> (G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T))\<and>
+                    (s\<le>|snd (the_In2 v)\<preceq>T\<Colon>\<preceq>(G,L))
+                else G,s\<turnstile>the_In1 v\<Colon>\<preceq>T
+    | Inr Ts \<Rightarrow> list_all2 (conf G s) (the_In3 v) Ts)"
 
 text {*
  With @{term rconf} we describe the conformance of the result value of a term.
@@ -324,9 +328,11 @@
 
 declare fun_upd_apply [simp del]
 
-definition DynT_prop :: "[prog,inv_mode,qtname,ref_ty] \<Rightarrow> bool" ("_\<turnstile>_\<rightarrow>_\<preceq>_"[71,71,71,71]70) where
-  "G\<turnstile>mode\<rightarrow>D\<preceq>t \<equiv> mode = IntVir \<longrightarrow> is_class G D \<and> 
-                     (if (\<exists>T. t=ArrayT T) then D=Object else G\<turnstile>Class D\<preceq>RefT t)"
+definition
+  DynT_prop :: "[prog,inv_mode,qtname,ref_ty] \<Rightarrow> bool" ("_\<turnstile>_\<rightarrow>_\<preceq>_"[71,71,71,71]70)
+where
+  "G\<turnstile>mode\<rightarrow>D\<preceq>t = (mode = IntVir \<longrightarrow> is_class G D \<and> 
+                     (if (\<exists>T. t=ArrayT T) then D=Object else G\<turnstile>Class D\<preceq>RefT t))"
 
 lemma DynT_propI: 
  "\<lbrakk>(x,s)\<Colon>\<preceq>(G, L); G,s\<turnstile>a'\<Colon>\<preceq>RefT statT; wf_prog G; mode = IntVir \<longrightarrow> a' \<noteq> Null\<rbrakk> 
diff -r d9549f9da779 -r a79abb22ca9c src/HOL/Bali/Value.thy
--- a/src/HOL/Bali/Value.thy	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/Value.thy	Mon Jul 26 18:25:19 2010 +0200
@@ -17,29 +17,34 @@
         | Addr loc      --{* addresses, i.e. locations of objects *}
 
 
-consts   the_Bool   :: "val \<Rightarrow> bool"  
-primrec "the_Bool (Bool b) = b"
-consts   the_Intg   :: "val \<Rightarrow> int"
-primrec "the_Intg (Intg i) = i"
-consts   the_Addr   :: "val \<Rightarrow> loc"
-primrec "the_Addr (Addr a) = a"
+primrec the_Bool :: "val \<Rightarrow> bool"
+  where "the_Bool (Bool b) = b"
+
+primrec the_Intg :: "val \<Rightarrow> int"
+  where "the_Intg (Intg i) = i"
+
+primrec the_Addr :: "val \<Rightarrow> loc"
+  where "the_Addr (Addr a) = a"
 
 types   dyn_ty      = "loc \<Rightarrow> ty option"
-consts
-  typeof        :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option"
-  defpval       :: "prim_ty \<Rightarrow> val"  --{* default value for primitive types *}
-  default_val   :: "     ty \<Rightarrow> val"  --{* default value for all types *}
+
+primrec typeof :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option"
+where
+  "typeof dt  Unit = Some (PrimT Void)"
+| "typeof dt (Bool b) = Some (PrimT Boolean)"
+| "typeof dt (Intg i) = Some (PrimT Integer)"
+| "typeof dt  Null = Some NT"
+| "typeof dt (Addr a) = dt a"
 
-primrec "typeof dt  Unit    = Some (PrimT Void)"
-        "typeof dt (Bool b) = Some (PrimT Boolean)"
-        "typeof dt (Intg i) = Some (PrimT Integer)"
-        "typeof dt  Null    = Some NT"
-        "typeof dt (Addr a) = dt a"
+primrec defpval :: "prim_ty \<Rightarrow> val"  --{* default value for primitive types *}
+where
+  "defpval Void = Unit"
+| "defpval Boolean = Bool False"
+| "defpval Integer = Intg 0"
 
-primrec "defpval Void    = Unit"
-        "defpval Boolean = Bool False"
-        "defpval Integer = Intg 0"
-primrec "default_val (PrimT pt) = defpval pt"
-        "default_val (RefT  r ) = Null"
+primrec default_val :: "ty \<Rightarrow> val"  --{* default value for all types *}
+where
+  "default_val (PrimT pt) = defpval pt"
+| "default_val (RefT  r ) = Null"
 
 end
diff -r d9549f9da779 -r a79abb22ca9c src/HOL/Bali/WellForm.thy
--- a/src/HOL/Bali/WellForm.thy	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/WellForm.thy	Mon Jul 26 18:25:19 2010 +0200
@@ -31,8 +31,9 @@
 text  {* well-formed field declaration (common part for classes and interfaces),
         cf. 8.3 and (9.3) *}
 
-definition wf_fdecl :: "prog \<Rightarrow> pname \<Rightarrow> fdecl \<Rightarrow> bool" where
- "wf_fdecl G P \<equiv> \<lambda>(fn,f). is_acc_type G P (type f)"
+definition
+  wf_fdecl :: "prog \<Rightarrow> pname \<Rightarrow> fdecl \<Rightarrow> bool"
+  where "wf_fdecl G P = (\<lambda>(fn,f). is_acc_type G P (type f))"
 
 lemma wf_fdecl_def2: "\<And>fd. wf_fdecl G P fd = is_acc_type G P (type (snd fd))"
 apply (unfold wf_fdecl_def)
@@ -54,11 +55,12 @@
 \item the parameter names are unique
 \end{itemize} 
 *}
-definition wf_mhead :: "prog \<Rightarrow> pname \<Rightarrow> sig \<Rightarrow> mhead \<Rightarrow> bool" where
- "wf_mhead G P \<equiv> \<lambda> sig mh. length (parTs sig) = length (pars mh) \<and>
+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> 
                             is_acc_type G P (resTy mh) \<and>
-                            \<spacespace> distinct (pars mh)"
+                            \<spacespace> distinct (pars mh))"
 
 
 text {*
@@ -76,23 +78,25 @@
 \end{itemize}
 *}
 
-definition callee_lcl :: "qtname \<Rightarrow> sig \<Rightarrow> methd \<Rightarrow> lenv" where
-"callee_lcl C sig m 
- \<equiv> \<lambda> k. (case k of
+definition
+  callee_lcl :: "qtname \<Rightarrow> sig \<Rightarrow> methd \<Rightarrow> lenv" where
+  "callee_lcl C sig m =
+    (\<lambda>k. (case k of
             EName e 
             \<Rightarrow> (case e of 
                   VNam v 
                   \<Rightarrow>(table_of (lcls (mbody m))((pars m)[\<mapsto>](parTs sig))) v
                 | Res \<Rightarrow> Some (resTy m))
-          | This \<Rightarrow> if is_static m then None else Some (Class C))"
+          | This \<Rightarrow> if is_static m then None else Some (Class C)))"
 
-definition parameters :: "methd \<Rightarrow> lname set" where
-"parameters m \<equiv>  set (map (EName \<circ> VNam) (pars m)) 
-                  \<union> (if (static m) then {} else {This})"
+definition
+  parameters :: "methd \<Rightarrow> lname set" where
+  "parameters m = set (map (EName \<circ> VNam) (pars m)) \<union> (if (static m) then {} else {This})"
 
-definition wf_mdecl :: "prog \<Rightarrow> qtname \<Rightarrow> mdecl \<Rightarrow> bool" where
- "wf_mdecl G C \<equiv> 
-      \<lambda>(sig,m).
+definition
+  wf_mdecl :: "prog \<Rightarrow> qtname \<Rightarrow> mdecl \<Rightarrow> bool" where
+  "wf_mdecl G C =
+      (\<lambda>(sig,m).
           wf_mhead G (pid C) sig (mhead m) \<and> 
           unique (lcls (mbody m)) \<and> 
           (\<forall>(vn,T)\<in>set (lcls (mbody m)). is_acc_type G (pid C) T) \<and> 
@@ -102,7 +106,7 @@
           \<lparr>prg=G,cls=C,lcl=callee_lcl C sig m\<rparr>\<turnstile>(stmt (mbody m))\<Colon>\<surd> \<and>
           (\<exists> A. \<lparr>prg=G,cls=C,lcl=callee_lcl C sig m\<rparr> 
                 \<turnstile> parameters m \<guillemotright>\<langle>stmt (mbody m)\<rangle>\<guillemotright> A 
-               \<and> Result \<in> nrm A)"
+               \<and> Result \<in> nrm A))"
 
 lemma callee_lcl_VNam_simp [simp]:
 "callee_lcl C sig m (EName (VNam v)) 
@@ -216,9 +220,10 @@
       superinterfaces widens to each of the corresponding result types
 \end{itemize}
 *}
-definition wf_idecl :: "prog  \<Rightarrow> idecl \<Rightarrow> bool" where
- "wf_idecl G \<equiv> 
-    \<lambda>(I,i). 
+definition
+  wf_idecl :: "prog  \<Rightarrow> idecl \<Rightarrow> bool" where
+ "wf_idecl G =
+    (\<lambda>(I,i). 
         ws_idecl G I (isuperIfs i) \<and> 
         \<not>is_class G I \<and>
         (\<forall>(sig,mh)\<in>set (imethods i). wf_mhead G (pid I) sig mh \<and> 
@@ -233,7 +238,7 @@
                              is_static new = is_static old)) \<and> 
         (Option.set \<circ> table_of (imethods i) 
                hidings Un_tables((\<lambda>J.(imethds G J))`set (isuperIfs i))
-               entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old))"
+               entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old)))"
 
 lemma wf_idecl_mhead: "\<lbrakk>wf_idecl G (I,i); (sig,mh)\<in>set (imethods i)\<rbrakk> \<Longrightarrow>  
   wf_mhead G (pid I) sig mh \<and> \<not>is_static mh \<and> accmodi mh = Public"
@@ -317,8 +322,9 @@
 \end{itemize}
 *}
 (* to Table *)
-definition entails :: "('a,'b) table \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool" ("_ entails _" 20) where
-"t entails P \<equiv> \<forall>k. \<forall> x \<in> t k: P x"
+definition
+  entails :: "('a,'b) table \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool" ("_ entails _" 20)
+  where "(t entails P) = (\<forall>k. \<forall> x \<in> t k: P x)"
 
 lemma entailsD:
  "\<lbrakk>t entails P; t k = Some x\<rbrakk> \<Longrightarrow> P x"
@@ -327,9 +333,10 @@
 lemma empty_entails[simp]: "empty entails P"
 by (simp add: entails_def)
 
-definition wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool" where
-"wf_cdecl G \<equiv> 
-   \<lambda>(C,c).
+definition
+  wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool" where
+  "wf_cdecl G =
+     (\<lambda>(C,c).
       \<not>is_iface G C \<and>
       (\<forall>I\<in>set (superIfs c). is_acc_iface G (pid C) I \<and>
         (\<forall>s. \<forall> im \<in> imethds G I s.
@@ -352,7 +359,7 @@
                        (G,sig\<turnstile>new hides old 
                          \<longrightarrow> (accmodi old \<le> accmodi new \<and>
                               is_static old)))) 
-            ))"
+            )))"
 
 (*
 definition wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool" where
@@ -511,13 +518,14 @@
 \item all defined classes are wellformed
 \end{itemize}
 *}
-definition wf_prog :: "prog \<Rightarrow> bool" where
- "wf_prog G \<equiv> let is = ifaces G; cs = classes G in
+definition
+  wf_prog :: "prog \<Rightarrow> bool" where
+ "wf_prog G = (let is = ifaces G; cs = classes G in
                  ObjectC \<in> set cs \<and> 
                 (\<forall> m\<in>set Object_mdecls. accmodi m \<noteq> Package) \<and>
                 (\<forall>xn. SXcptC xn \<in> set cs) \<and>
                 (\<forall>i\<in>set is. wf_idecl G i) \<and> unique is \<and>
-                (\<forall>c\<in>set cs. wf_cdecl G c) \<and> unique cs"
+                (\<forall>c\<in>set cs. wf_cdecl G c) \<and> unique cs)"
 
 lemma wf_prog_idecl: "\<lbrakk>iface G I = Some i; wf_prog G\<rbrakk> \<Longrightarrow> wf_idecl G (I,i)"
 apply (unfold wf_prog_def Let_def)
@@ -2095,16 +2103,16 @@
  Class    dynC 
  Array    Object
 *}
-consts valid_lookup_cls:: "prog \<Rightarrow> ref_ty \<Rightarrow> qtname \<Rightarrow> bool \<Rightarrow> bool"
+primrec valid_lookup_cls:: "prog \<Rightarrow> ref_ty \<Rightarrow> qtname \<Rightarrow> bool \<Rightarrow> bool"
                         ("_,_ \<turnstile> _ valid'_lookup'_cls'_for _" [61,61,61,61] 60)
-primrec
-"G,NullT    \<turnstile> dynC valid_lookup_cls_for static_membr = False"
-"G,IfaceT I \<turnstile> dynC valid_lookup_cls_for static_membr 
-              = (if static_membr 
-                    then dynC=Object 
-                    else G\<turnstile>Class dynC\<preceq> Iface I)"
-"G,ClassT C \<turnstile> dynC valid_lookup_cls_for static_membr = G\<turnstile>Class dynC\<preceq> Class C"
-"G,ArrayT T \<turnstile> dynC valid_lookup_cls_for static_membr = (dynC=Object)"
+where
+  "G,NullT    \<turnstile> dynC valid_lookup_cls_for static_membr = False"
+| "G,IfaceT I \<turnstile> dynC valid_lookup_cls_for static_membr 
+                = (if static_membr 
+                      then dynC=Object 
+                      else G\<turnstile>Class dynC\<preceq> Iface I)"
+| "G,ClassT C \<turnstile> dynC valid_lookup_cls_for static_membr = G\<turnstile>Class dynC\<preceq> Class C"
+| "G,ArrayT T \<turnstile> dynC valid_lookup_cls_for static_membr = (dynC=Object)"
 
 lemma valid_lookup_cls_is_class:
   assumes dynC: "G,statT \<turnstile> dynC valid_lookup_cls_for static_membr" and
diff -r d9549f9da779 -r a79abb22ca9c src/HOL/Bali/WellType.thy
--- a/src/HOL/Bali/WellType.thy	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/WellType.thy	Mon Jul 26 18:25:19 2010 +0200
@@ -53,11 +53,13 @@
   emhead = "ref_ty \<times> mhead"
 
 --{* Some mnemotic selectors for emhead *}
-definition "declrefT" :: "emhead \<Rightarrow> ref_ty" where
-  "declrefT \<equiv> fst"
+definition
+  "declrefT" :: "emhead \<Rightarrow> ref_ty"
+  where "declrefT = fst"
 
-definition "mhd"     :: "emhead \<Rightarrow> mhead" where
-  "mhd \<equiv> snd"
+definition
+  "mhd" :: "emhead \<Rightarrow> mhead"
+  where "mhd \<equiv> snd"
 
 lemma declrefT_simp[simp]:"declrefT (r,m) = r"
 by (simp add: declrefT_def)
@@ -77,50 +79,51 @@
 lemma mhd_accmodi_simp [simp]: "accmodi (mhd m) = accmodi m"
 by (cases m) simp
 
-consts
-  cmheads        :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set"
-  Objectmheads   :: "prog \<Rightarrow> qtname           \<Rightarrow> sig \<Rightarrow> emhead set"
-  accObjectmheads:: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
-  mheads         :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
-defs
- cmheads_def:
-"cmheads G S C 
-  \<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` Option.set (accmethd G S C sig)"
-  Objectmheads_def:
-"Objectmheads G S  
-  \<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) 
-    ` Option.set (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig)"
-  accObjectmheads_def:
-"accObjectmheads G S T
-   \<equiv> if G\<turnstile>RefT T accessible_in (pid S)
-        then Objectmheads G S
-        else (\<lambda>sig. {})"
-primrec
-"mheads G S  NullT     = (\<lambda>sig. {})"
-"mheads G S (IfaceT I) = (\<lambda>sig. (\<lambda>(I,h).(IfaceT I,h)) 
-                         ` accimethds G (pid S) I sig \<union> 
-                           accObjectmheads G S (IfaceT I) sig)"
-"mheads G S (ClassT C) = cmheads G S C"
-"mheads G S (ArrayT T) = accObjectmheads G S (ArrayT T)"
+definition
+  cmheads :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set"
+  where "cmheads G S C = (\<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` Option.set (accmethd G S C sig))"
+
+definition
+  Objectmheads :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set" where
+  "Objectmheads G S =
+    (\<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) 
+      ` Option.set (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig))"
+
+definition
+  accObjectmheads :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
+where
+  "accObjectmheads G S T =
+    (if G\<turnstile>RefT T accessible_in (pid S)
+     then Objectmheads G S
+     else (\<lambda>sig. {}))"
+
+primrec mheads :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
+where
+  "mheads G S  NullT     = (\<lambda>sig. {})"
+| "mheads G S (IfaceT I) = (\<lambda>sig. (\<lambda>(I,h).(IfaceT I,h)) 
+                           ` accimethds G (pid S) I sig \<union> 
+                             accObjectmheads G S (IfaceT I) sig)"
+| "mheads G S (ClassT C) = cmheads G S C"
+| "mheads G S (ArrayT T) = accObjectmheads G S (ArrayT T)"
 
 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 G S rt = (\<lambda> sig. 
+  appl_methds :: "prog \<Rightarrow> qtname \<Rightarrow>  ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> 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'})"
 
 definition
   --{* more specific methods, cf. 15.11.2.2 *}
-  more_spec     :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool" where
- "more_spec G = (\<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs')"
+  more_spec :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool" where
+  "more_spec G = (\<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs')"
 (*more_spec G \<equiv>\<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>RefT d\<preceq>RefT d'\<and>G\<turnstile>pTs[\<preceq>]pTs'*)
 
 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 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)}"
+  max_spec :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> 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)}"
 
 
 lemma max_spec2appl_meths: 
@@ -138,13 +141,15 @@
 done
 
 
-definition empty_dt :: "dyn_ty" where
- "empty_dt \<equiv> \<lambda>a. None"
+definition
+  empty_dt :: "dyn_ty"
+  where "empty_dt = (\<lambda>a. None)"
 
-definition invmode :: "('a::type)member_scheme \<Rightarrow> expr \<Rightarrow> inv_mode" where
-"invmode m e \<equiv> if is_static m 
+definition
+  invmode :: "('a::type)member_scheme \<Rightarrow> expr \<Rightarrow> inv_mode" where
+  "invmode m e = (if is_static m 
                   then Static 
-                  else if e=Super then SuperM else IntVir"
+                  else if e=Super then SuperM else IntVir)"
 
 lemma invmode_nonstatic [simp]: 
   "invmode \<lparr>access=a,static=False,\<dots>=x\<rparr> (Acc (LVar e)) = IntVir"
@@ -171,71 +176,71 @@
 
 section "Typing for unary operations"
 
-consts unop_type :: "unop \<Rightarrow> prim_ty"
-primrec 
-"unop_type UPlus   = Integer"
-"unop_type UMinus  = Integer"
-"unop_type UBitNot = Integer"
-"unop_type UNot    = Boolean"    
+primrec unop_type :: "unop \<Rightarrow> prim_ty"
+where
+  "unop_type UPlus   = Integer"
+| "unop_type UMinus  = Integer"
+| "unop_type UBitNot = Integer"
+| "unop_type UNot    = Boolean"    
 
-consts wt_unop :: "unop \<Rightarrow> ty \<Rightarrow> bool"
-primrec
-"wt_unop UPlus   t = (t = PrimT Integer)"
-"wt_unop UMinus  t = (t = PrimT Integer)"
-"wt_unop UBitNot t = (t = PrimT Integer)"
-"wt_unop UNot    t = (t = PrimT Boolean)"
+primrec wt_unop :: "unop \<Rightarrow> ty \<Rightarrow> bool"
+where
+  "wt_unop UPlus   t = (t = PrimT Integer)"
+| "wt_unop UMinus  t = (t = PrimT Integer)"
+| "wt_unop UBitNot t = (t = PrimT Integer)"
+| "wt_unop UNot    t = (t = PrimT Boolean)"
 
 section "Typing for binary operations"
 
-consts binop_type :: "binop \<Rightarrow> prim_ty"
-primrec
-"binop_type Mul      = Integer"     
-"binop_type Div      = Integer"
-"binop_type Mod      = Integer"
-"binop_type Plus     = Integer"
-"binop_type Minus    = Integer"
-"binop_type LShift   = Integer"
-"binop_type RShift   = Integer"
-"binop_type RShiftU  = Integer"
-"binop_type Less     = Boolean"
-"binop_type Le       = Boolean"
-"binop_type Greater  = Boolean"
-"binop_type Ge       = Boolean"
-"binop_type Eq       = Boolean"
-"binop_type Neq      = Boolean"
-"binop_type BitAnd   = Integer"
-"binop_type And      = Boolean"
-"binop_type BitXor   = Integer"
-"binop_type Xor      = Boolean"
-"binop_type BitOr    = Integer"
-"binop_type Or       = Boolean"
-"binop_type CondAnd  = Boolean"
-"binop_type CondOr   = Boolean"
+primrec binop_type :: "binop \<Rightarrow> prim_ty"
+where
+  "binop_type Mul      = Integer"     
+| "binop_type Div      = Integer"
+| "binop_type Mod      = Integer"
+| "binop_type Plus     = Integer"
+| "binop_type Minus    = Integer"
+| "binop_type LShift   = Integer"
+| "binop_type RShift   = Integer"
+| "binop_type RShiftU  = Integer"
+| "binop_type Less     = Boolean"
+| "binop_type Le       = Boolean"
+| "binop_type Greater  = Boolean"
+| "binop_type Ge       = Boolean"
+| "binop_type Eq       = Boolean"
+| "binop_type Neq      = Boolean"
+| "binop_type BitAnd   = Integer"
+| "binop_type And      = Boolean"
+| "binop_type BitXor   = Integer"
+| "binop_type Xor      = Boolean"
+| "binop_type BitOr    = Integer"
+| "binop_type Or       = Boolean"
+| "binop_type CondAnd  = Boolean"
+| "binop_type CondOr   = Boolean"
 
-consts wt_binop :: "prog \<Rightarrow> binop \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"
-primrec
-"wt_binop G Mul     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G Div     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G Mod     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G Plus    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G Minus   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G LShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G RShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G RShiftU t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G Less    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G Le      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G Greater t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G Ge      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G Eq      t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)" 
-"wt_binop G Neq     t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)"
-"wt_binop G BitAnd  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G And     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
-"wt_binop G BitXor  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G Xor     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
-"wt_binop G BitOr   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G Or      t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
-"wt_binop G CondAnd t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
-"wt_binop G CondOr  t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
+primrec wt_binop :: "prog \<Rightarrow> binop \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"
+where
+  "wt_binop G Mul     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G Div     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G Mod     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G Plus    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G Minus   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G LShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G RShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G RShiftU t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G Less    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G Le      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G Greater t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G Ge      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G Eq      t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)" 
+| "wt_binop G Neq     t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)"
+| "wt_binop G BitAnd  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G And     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
+| "wt_binop G BitXor  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G Xor     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
+| "wt_binop G BitOr   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G Or      t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
+| "wt_binop G CondAnd t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
+| "wt_binop G CondOr  t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
 
 section "Typing for terms"
 
@@ -244,9 +249,8 @@
   (type) "tys" <= (type) "ty + ty list"
 
 
-inductive
-  wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_"  [51,51,51,51] 50)
-  and wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow>  stmt       \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>"  [51,51,51   ] 50)
+inductive wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_"  [51,51,51,51] 50)
+  and wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow>  stmt       \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>"  [51,51,51] 50)
   and ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>-_" [51,51,51,51] 50)
   and ty_var :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>=_" [51,51,51,51] 50)
   and ty_exprs :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list, ty   list] \<Rightarrow> bool"
diff -r d9549f9da779 -r a79abb22ca9c src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Tools/inductive.ML	Mon Jul 26 18:25:19 2010 +0200
@@ -522,9 +522,9 @@
 fun gen_inductive_cases prep_att prep_prop args lthy =
   let
     val thy = ProofContext.theory_of lthy;
-    val facts = args |> map (fn ((a, atts), props) =>
+    val facts = args |> Par_List.map (fn ((a, atts), props) =>
       ((a, map (prep_att thy) atts),
-        map (Thm.no_attributes o single o mk_cases lthy o prep_prop lthy) props));
+        Par_List.map (Thm.no_attributes o single o mk_cases lthy o prep_prop lthy) props));
   in lthy |> Local_Theory.notes facts |>> map snd end;
 
 val inductive_cases = gen_inductive_cases Attrib.intern_src Syntax.read_prop;
diff -r d9549f9da779 -r a79abb22ca9c src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Mon Jul 26 18:25:19 2010 +0200
@@ -274,10 +274,8 @@
 (* init and exit *)
 
 fun init_theory (name, imports, uses) =
-  Toplevel.init_theory name (Thy_Info.begin_theory name imports (map (apfst Path.explode) uses))
-    (fn thy =>
-      if Thy_Info.check_known_thy (Context.theory_name thy)
-      then Thy_Info.end_theory thy else ());
+  Toplevel.init_theory name
+    (Thy_Info.begin_theory name imports (map (apfst Path.explode) uses));
 
 val exit = Toplevel.keep (fn state =>
  (Context.set_thread_data (try Toplevel.generic_theory_of state);
diff -r d9549f9da779 -r a79abb22ca9c src/Pure/Isar/isar_document.ML
--- a/src/Pure/Isar/isar_document.ML	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/Pure/Isar/isar_document.ML	Mon Jul 26 18:25:19 2010 +0200
@@ -181,7 +181,7 @@
 
 fun begin_document (id: document_id) path =
   let
-    val (dir, name) = Thy_Load.split_thy_path path;
+    val (dir, name) = Thy_Header.split_thy_path path;
     val _ = define_document id (make_document dir name no_entries);
   in () end;
 
@@ -192,13 +192,10 @@
       val end_state =
         the_state (the (#state (#3 (the
           (first_entry (fn (_, {next, ...}) => is_none next) document)))));
-      val _ =  (* FIXME regular execution (??) *)
+      val _ =  (* FIXME regular execution (??), result (??) *)
         Future.fork (fn () =>
           (case Lazy.force end_state of
-            SOME st =>
-             (Toplevel.run_command name (Toplevel.put_id id (Toplevel.commit_exit Position.none)) st;
-              Thy_Info.touch_child_thys name;
-              Thy_Info.register_thy name)
+            SOME st => Toplevel.end_theory (Position.id_only id) st
           | NONE => error ("Failed to finish theory " ^ quote name)));
     in () end);
 
diff -r d9549f9da779 -r a79abb22ca9c src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon Jul 26 18:25:19 2010 +0200
@@ -304,30 +304,23 @@
 
 (* use ML text *)
 
-fun propagate_env (context as Context.Proof lthy) =
-      Context.Proof (Local_Theory.map_contexts (ML_Env.inherit context) lthy)
-  | propagate_env context = context;
-
-fun propagate_env_prf prf = Proof.map_contexts
-  (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf;
-
 val _ =
   Outer_Syntax.command "use" "ML text from file" (Keyword.tag_ml Keyword.thy_decl)
-    (Parse.path >>
-      (fn path => Toplevel.generic_theory (Thy_Info.exec_file path #> propagate_env)));
+    (Parse.path >> (fn path => Toplevel.generic_theory (Thy_Load.exec_ml path)));
 
 val _ =
   Outer_Syntax.command "ML" "ML text within theory or local theory"
     (Keyword.tag_ml Keyword.thy_decl)
     (Parse.ML_source >> (fn (txt, pos) =>
       Toplevel.generic_theory
-        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt) #> propagate_env)));
+        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt) #>
+          Local_Theory.propagate_ml_env)));
 
 val _ =
   Outer_Syntax.command "ML_prf" "ML text within proof" (Keyword.tag_proof Keyword.prf_decl)
     (Parse.ML_source >> (fn (txt, pos) =>
       Toplevel.proof (Proof.map_context (Context.proof_map
-        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> propagate_env_prf)));
+        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> Proof.propagate_ml_env)));
 
 val _ =
   Outer_Syntax.command "ML_val" "diagnostic ML text" (Keyword.tag_ml Keyword.diag)
diff -r d9549f9da779 -r a79abb22ca9c src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/Pure/Isar/local_theory.ML	Mon Jul 26 18:25:19 2010 +0200
@@ -5,6 +5,7 @@
 *)
 
 type local_theory = Proof.context;
+type generic_theory = Context.generic;
 
 signature LOCAL_THEORY =
 sig
@@ -25,6 +26,7 @@
   val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
   val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
   val map_contexts: (Context.generic -> Context.generic) -> local_theory -> local_theory
+  val propagate_ml_env: generic_theory -> generic_theory
   val standard_morphism: local_theory -> Proof.context -> morphism
   val target_morphism: local_theory -> morphism
   val global_morphism: local_theory -> morphism
@@ -173,6 +175,10 @@
   target (Context.proof_map f) #>
   Context.proof_map f;
 
+fun propagate_ml_env (context as Context.Proof lthy) =
+      Context.Proof (map_contexts (ML_Env.inherit context) lthy)
+  | propagate_ml_env context = context;
+
 
 (* morphisms *)
 
diff -r d9549f9da779 -r a79abb22ca9c src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Jul 26 18:25:19 2010 +0200
@@ -31,7 +31,7 @@
   type isar
   val isar: bool -> isar
   val prepare_command: Position.T -> string -> Toplevel.transition
-  val load_thy: string -> Position.T -> string -> unit -> unit
+  val load_thy: string -> Position.T -> string -> (unit -> unit) * theory
 end;
 
 structure Outer_Syntax: OUTER_SYNTAX =
@@ -204,7 +204,7 @@
 fun process_file path thy =
   let
     val trs = parse (Path.position path) (File.read path);
-    val init = Toplevel.init_theory "" (K thy) (K ()) Toplevel.empty;
+    val init = Toplevel.init_theory "" (K thy) Toplevel.empty;
     val result = fold Toplevel.command (init :: trs) Toplevel.toplevel;
   in
     (case (Toplevel.is_theory result, Toplevel.generic_theory_of result) of
@@ -285,14 +285,14 @@
       (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
 
     val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
-    val results = cond_timeit time "" (fn () => Toplevel.excursion units);
+    val (results, thy) = cond_timeit time "" (fn () => Toplevel.excursion units);
     val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
 
     fun after_load () =
       Thy_Output.present_thy (#1 lexs) Keyword.command_tags is_markup (Lazy.force results) toks
       |> Buffer.content
       |> Present.theory_output name;
-  in after_load end;
+  in (after_load, thy) end;
 
 end;
 
diff -r d9549f9da779 -r a79abb22ca9c src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/Pure/Isar/proof.ML	Mon Jul 26 18:25:19 2010 +0200
@@ -17,6 +17,7 @@
   val theory_of: state -> theory
   val map_context: (context -> context) -> state -> state
   val map_contexts: (context -> context) -> state -> state
+  val propagate_ml_env: state -> state
   val bind_terms: (indexname * term option) list -> state -> state
   val put_thms: bool -> string * thm list option -> state -> state
   val the_facts: state -> thm list
@@ -207,6 +208,9 @@
 
 fun map_contexts f = map_all (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
 
+fun propagate_ml_env state = map_contexts
+  (Context.proof_map (ML_Env.inherit (Context.Proof (context_of state)))) state;
+
 val bind_terms = map_context o ProofContext.bind_terms;
 val put_thms = map_context oo ProofContext.put_thms;
 
diff -r d9549f9da779 -r a79abb22ca9c src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Mon Jul 26 18:25:19 2010 +0200
@@ -7,7 +7,6 @@
 signature TOPLEVEL =
 sig
   exception UNDEF
-  type generic_theory
   type state
   val toplevel: state
   val is_toplevel: state -> bool
@@ -22,6 +21,7 @@
   val proof_of: state -> Proof.state
   val proof_position_of: state -> int
   val enter_proof_body: state -> Proof.state
+  val end_theory: Position.T -> state -> theory
   val print_state_context: state -> unit
   val print_state: bool -> state -> unit
   val pretty_abstract: state -> Pretty.T
@@ -46,7 +46,7 @@
   val interactive: bool -> transition -> transition
   val print: transition -> transition
   val no_timing: transition -> transition
-  val init_theory: string -> (bool -> theory) -> (theory -> unit) -> transition -> transition
+  val init_theory: string -> (bool -> theory) -> transition -> transition
   val exit: transition -> transition
   val keep: (state -> unit) -> transition -> transition
   val keep': (bool -> state -> unit) -> transition -> transition
@@ -88,9 +88,8 @@
   val add_hook: (transition -> state -> state -> unit) -> unit
   val transition: bool -> transition -> state -> (state * (exn * string) option) option
   val run_command: string -> transition -> state -> state option
-  val commit_exit: Position.T -> transition
   val command: transition -> state -> state
-  val excursion: (transition * transition list) list -> (transition * state) list lazy
+  val excursion: (transition * transition list) list -> (transition * state) list lazy * theory
 end;
 
 structure Toplevel: TOPLEVEL =
@@ -103,8 +102,6 @@
 
 (* local theory wrappers *)
 
-type generic_theory = Context.generic;    (*theory or local_theory*)
-
 val loc_init = Theory_Target.context_cmd;
 val loc_exit = Local_Theory.exit_global;
 
@@ -140,8 +137,7 @@
 
 (* datatype state *)
 
-type node_info = node * (theory -> unit);  (*node with exit operation*)
-datatype state = State of node_info option * node_info option;  (*current, previous*)
+datatype state = State of node option * node option;  (*current, previous*)
 
 val toplevel = State (NONE, NONE);
 
@@ -149,21 +145,21 @@
   | is_toplevel _ = false;
 
 fun level (State (NONE, _)) = 0
-  | level (State (SOME (Theory _, _), _)) = 0
-  | level (State (SOME (Proof (prf, _), _), _)) = Proof.level (Proof_Node.current prf)
-  | level (State (SOME (SkipProof (d, _), _), _)) = d + 1;   (*different notion of proof depth!*)
+  | level (State (SOME (Theory _), _)) = 0
+  | level (State (SOME (Proof (prf, _)), _)) = Proof.level (Proof_Node.current prf)
+  | level (State (SOME (SkipProof (d, _)), _)) = d + 1;   (*different notion of proof depth!*)
 
 fun str_of_state (State (NONE, _)) = "at top level"
-  | str_of_state (State (SOME (Theory (Context.Theory _, _), _), _)) = "in theory mode"
-  | str_of_state (State (SOME (Theory (Context.Proof _, _), _), _)) = "in local theory mode"
-  | str_of_state (State (SOME (Proof _, _), _)) = "in proof mode"
-  | str_of_state (State (SOME (SkipProof _, _), _)) = "in skipped proof mode";
+  | str_of_state (State (SOME (Theory (Context.Theory _, _)), _)) = "in theory mode"
+  | str_of_state (State (SOME (Theory (Context.Proof _, _)), _)) = "in local theory mode"
+  | str_of_state (State (SOME (Proof _), _)) = "in proof mode"
+  | str_of_state (State (SOME (SkipProof _), _)) = "in skipped proof mode";
 
 
 (* current node *)
 
 fun node_of (State (NONE, _)) = raise UNDEF
-  | node_of (State (SOME (node, _), _)) = node;
+  | node_of (State (SOME node, _)) = node;
 
 fun is_theory state = not (is_toplevel state) andalso is_some (theory_node (node_of state));
 fun is_proof state = not (is_toplevel state) andalso is_some (proof_node (node_of state));
@@ -177,7 +173,7 @@
   | NONE => raise UNDEF);
 
 fun previous_context_of (State (_, NONE)) = NONE
-  | previous_context_of (State (_, SOME (prev, _))) = SOME (context_node prev);
+  | previous_context_of (State (_, SOME prev)) = SOME (context_node prev);
 
 val context_of = node_case Context.proof_of Proof.context_of;
 val generic_theory_of = node_case I (Context.Proof o Proof.context_of);
@@ -191,6 +187,9 @@
 
 val enter_proof_body = node_case (Proof.init o Context.proof_of) Proof.enter_forward;
 
+fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = Theory.end_theory thy
+  | end_theory pos _ = error ("Unfinished theory at end of input" ^ Position.str_of pos);
+
 
 (* print state *)
 
@@ -267,12 +266,12 @@
 
 in
 
-fun apply_transaction f g (node, exit) =
+fun apply_transaction f g node =
   let
     val _ = is_draft_theory node andalso error "Illegal draft theory in toplevel state";
     val cont_node = reset_presentation node;
     val back_node = map_theory (Theory.checkpoint o Theory.copy) cont_node;
-    fun state_error e nd = (State (SOME (nd, exit), SOME (node, exit)), e);
+    fun state_error e nd = (State (SOME nd, SOME node), e);
 
     val (result, err) =
       cont_node
@@ -296,21 +295,18 @@
 (* primitive transitions *)
 
 datatype trans =
-  Init of string * (bool -> theory) * (theory -> unit) | (*theory name, init, exit*)
-  Exit |                                         (*formal exit of theory -- without committing*)
-  CommitExit |                                   (*exit and commit final theory*)
-  Keep of bool -> state -> unit |                (*peek at state*)
+  Init of string * (bool -> theory) |    (*theory name, init*)
+  Exit |                                 (*formal exit of theory*)
+  Keep of bool -> state -> unit |        (*peek at state*)
   Transaction of (bool -> node -> node) * (state -> unit);  (*node transaction and presentation*)
 
 local
 
-fun apply_tr int (Init (_, f, exit)) (State (NONE, _)) =
+fun apply_tr int (Init (_, f)) (State (NONE, _)) =
       State (SOME (Theory (Context.Theory
-          (Theory.checkpoint (Runtime.controlled_execution f int)), NONE), exit), NONE)
-  | apply_tr _ Exit (State (prev as SOME (Theory (Context.Theory _, _), _), _)) =
+          (Theory.checkpoint (Runtime.controlled_execution f int)), NONE)), NONE)
+  | apply_tr _ Exit (State (prev as SOME (Theory (Context.Theory _, _)), _)) =
       State (NONE, prev)
-  | apply_tr _ CommitExit (State (NONE, SOME (Theory (Context.Theory thy, _), exit))) =
-      (Runtime.controlled_execution exit thy; toplevel)
   | apply_tr int (Keep f) state =
       Runtime.controlled_execution (fn x => tap (f int) x) state
   | apply_tr int (Transaction (f, g)) (State (SOME state, _)) =
@@ -355,7 +351,7 @@
 
 (* diagnostics *)
 
-fun init_of (Transition {trans = [Init (name, _, _)], ...}) = SOME name
+fun init_of (Transition {trans = [Init (name, _)], ...}) = SOME name
   | init_of _ = NONE;
 
 fun name_of (Transition {name, ...}) = name;
@@ -397,7 +393,7 @@
 
 (* basic transitions *)
 
-fun init_theory name f exit = add_trans (Init (name, f, exit));
+fun init_theory name f = add_trans (Init (name, f));
 val exit = add_trans Exit;
 val keep' = add_trans o Keep;
 
@@ -632,7 +628,7 @@
 fun run_command thy_name tr st =
   (case
       (case init_of tr of
-        SOME name => Exn.capture (fn () => Thy_Load.consistent_name thy_name name) ()
+        SOME name => Exn.capture (fn () => Thy_Header.consistent_name thy_name name) ()
       | NONE => Exn.Result ()) of
     Exn.Result () =>
       let val int = is_some (init_of tr) in
@@ -646,15 +642,6 @@
   | Exn.Exn exn => (error_msg tr (exn, at_command tr); status tr Markup.failed; NONE));
 
 
-(* commit final exit *)
-
-fun commit_exit pos =
-  name "end" empty
-  |> position pos
-  |> add_trans CommitExit
-  |> imperative (fn () => warning "Expected to find finished theory");
-
-
 (* nested commands *)
 
 fun command tr st =
@@ -696,8 +683,8 @@
           (fn prf =>
             Future.fork_pri ~1 (fn () =>
               let val (states, result_state) =
-                (case st' of State (SOME (Proof (_, (_, orig_gthy)), exit), prev)
-                  => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy)), exit), prev))
+                (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
+                  => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
                 |> fold_map command_result body_trs
                 ||> command (end_tr |> set_print false);
               in (states, presentation_context_of result_state) end))
@@ -718,14 +705,9 @@
 fun excursion input =
   let
     val end_pos = if null input then error "No input" else pos_of (fst (List.last input));
-
     val immediate = not (Goal.future_enabled ());
     val (results, end_state) = fold_map (proof_result immediate) input toplevel;
-    val _ =
-      (case end_state of
-        State (NONE, SOME (Theory (Context.Theory _, _), _)) =>
-          command (commit_exit end_pos) end_state
-      | _ => error "Unfinished development at end of input");
-  in Lazy.lazy (fn () => maps Lazy.force results) end;
+    val thy = end_theory end_pos end_state;
+  in (Lazy.lazy (fn () => maps Lazy.force results), thy) end;
 
 end;
diff -r d9549f9da779 -r a79abb22ca9c src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Jul 26 18:25:19 2010 +0200
@@ -137,12 +137,11 @@
     val name = thy_name file;
     val _ = name = "" andalso error ("Bad file name: " ^ quote file);
     val _ =
-      if Thy_Info.check_known_thy name then
-        (Isar.>> (Toplevel.commit_exit Position.none);
-            Thy_Info.touch_child_thys name; Thy_Info.register_thy name)
+      if Thy_Info.known_thy name then
+        Thy_Info.register_thy (Toplevel.end_theory Position.none (Isar.state ()))
           handle ERROR msg =>
             (warning (cat_lines ["Failed to register theory: " ^ quote name, msg]);
-              tell_file_retracted (Thy_Load.thy_path name))
+              tell_file_retracted (Thy_Header.thy_path name))
       else ();
     val _ = Isar.init ();
   in () end;
diff -r d9549f9da779 -r a79abb22ca9c src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Jul 26 18:25:19 2010 +0200
@@ -218,15 +218,14 @@
 val thy_name = Path.implode o #1 o Path.split_ext o Path.base;
 
 val inform_file_retracted = Thy_Info.if_known_thy Thy_Info.remove_thy o thy_name;
-val inform_file_processed = Thy_Info.if_known_thy Thy_Info.touch_child_thys o thy_name;
 
-fun proper_inform_file_processed path state =
+fun inform_file_processed path state =
   let val name = thy_name path in
     if Toplevel.is_toplevel state andalso Thy_Info.known_thy name then
-     (Thy_Info.touch_child_thys name;
-      Thy_Info.register_thy name handle ERROR msg =>
-       (warning (cat_lines [msg, "Failed to register theory: " ^ quote name]);
-        tell_file_retracted true (Path.base path)))
+      Thy_Info.register_thy (Toplevel.end_theory Position.none state)
+        handle ERROR msg =>
+          (warning (cat_lines [msg, "Failed to register theory: " ^ quote name]);
+            tell_file_retracted true (Path.base path))
     else raise Toplevel.UNDEF
   end;
 
@@ -819,7 +818,7 @@
 
 fun closefile _ =
     case !currently_open_file of
-        SOME f => (proper_inform_file_processed f (Isar.state());
+        SOME f => (inform_file_processed f (Isar.state ());
                    priority ("Finished working in file: " ^ PgipTypes.string_of_pgipurl f);
                    currently_open_file := NONE)
       | NONE => raise PGIP ("<closefile> when no file is open!")
diff -r d9549f9da779 -r a79abb22ca9c src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/Pure/ROOT.ML	Mon Jul 26 18:25:19 2010 +0200
@@ -184,10 +184,8 @@
 
 (*theory sources*)
 use "Thy/thy_header.ML";
-use "Thy/thy_load.ML";
 use "Thy/html.ML";
 use "Thy/latex.ML";
-use "Thy/present.ML";
 
 (*basic proof engine*)
 use "Isar/proof_display.ML";
@@ -227,10 +225,12 @@
 use "Isar/constdefs.ML";
 
 (*toplevel transactions*)
+use "Thy/thy_load.ML";
 use "Isar/proof_node.ML";
 use "Isar/toplevel.ML";
 
 (*theory syntax*)
+use "Thy/present.ML";
 use "Thy/term_style.ML";
 use "Thy/thy_output.ML";
 use "Thy/thy_syntax.ML";
diff -r d9549f9da779 -r a79abb22ca9c src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/Pure/Thy/thy_header.ML	Mon Jul 26 18:25:19 2010 +0200
@@ -8,6 +8,9 @@
 sig
   val args: Token.T list -> (string * string list * (string * bool) list) * Token.T list
   val read: Position.T -> (string, 'a) Source.source -> string * string list * (string * bool) list
+  val thy_path: string -> Path.T
+  val split_thy_path: Path.T -> Path.T * string
+  val consistent_name: string -> string -> unit
 end;
 
 structure Thy_Header: THY_HEADER =
@@ -63,4 +66,19 @@
     | NONE => error ("Unexpected end of input" ^ Position.str_of pos))
   end;
 
+
+(* file formats *)
+
+val thy_path = Path.ext "thy" o Path.basic;
+
+fun split_thy_path path =
+  (case Path.split_ext path of
+    (path', "thy") => (Path.dir path', Path.implode (Path.base path'))
+  | _ => error ("Bad theory file specification " ^ Path.implode path));
+
+fun consistent_name name name' =
+  if name = name' then ()
+  else error ("Filename " ^ quote (Path.implode (thy_path name)) ^
+    " does not agree with theory name " ^ quote name');
+
 end;
diff -r d9549f9da779 -r a79abb22ca9c src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML	Mon Jul 26 18:25:19 2010 +0200
@@ -11,7 +11,6 @@
   val add_hook: (action -> string -> unit) -> unit
   val get_names: unit -> string list
   val known_thy: string -> bool
-  val check_known_thy: string -> bool
   val if_known_thy: (string -> unit) -> string -> unit
   val lookup_theory: string -> theory option
   val get_theory: string -> theory
@@ -19,20 +18,13 @@
   val master_directory: string -> Path.T
   val loaded_files: string -> Path.T list
   val touch_thy: string -> unit
-  val touch_child_thys: string -> unit
   val thy_ord: theory * theory -> order
   val remove_thy: string -> unit
   val kill_thy: string -> unit
-  val provide_file: Path.T -> string -> unit
-  val load_file: Path.T -> unit
-  val exec_file: Path.T -> Context.generic -> Context.generic
-  val use: string -> unit
   val use_thys: string list -> unit
   val use_thy: string -> unit
   val begin_theory: string -> string list -> (Path.T * bool) list -> bool -> theory
-  val end_theory: theory -> unit
-  val register_thy: string -> unit
-  val register_theory: theory -> unit
+  val register_thy: theory -> unit
   val finish: unit -> unit
 end;
 
@@ -80,18 +72,15 @@
 (* thy database *)
 
 type deps =
-  {update_time: int,                      (*symbolic time of update; negative value means outdated*)
-    master: (Path.T * File.ident) option, (*master dependencies for thy file*)
-    text: string,                         (*source text for thy*)
-    parents: string list,                 (*source specification of parents (partially qualified)*)
-      (*auxiliary files: source path, physical path + identifier*)
-    files: (Path.T * (Path.T * File.ident) option) list};
+ {update_time: int,                      (*symbolic time of update; negative value means outdated*)
+  master: (Path.T * File.ident) option,  (*master dependencies for thy file*)
+  text: string,                          (*source text for thy*)
+  parents: string list};                 (*source specification of parents (partially qualified)*)
 
-fun make_deps update_time master text parents files : deps =
-  {update_time = update_time, master = master, text = text, parents = parents, files = files};
+fun make_deps update_time master text parents : deps =
+  {update_time = update_time, master = master, text = text, parents = parents};
 
-fun init_deps master text parents files =
-  SOME (make_deps ~1 master text parents (map (rpair NONE) files));
+fun init_deps master text parents = SOME (make_deps ~1 master text parents);
 
 fun master_dir NONE = Path.current
   | master_dir (SOME (path, _)) = Path.dir path;
@@ -123,8 +112,7 @@
   SOME (thy_graph Graph.get_node name) handle Graph.UNDEF _ => NONE;
 
 val known_thy = is_some o lookup_thy;
-fun check_known_thy name = known_thy name orelse (warning ("Unknown theory " ^ quote name); false);
-fun if_known_thy f name = if check_known_thy name then f name else ();
+fun if_known_thy f name = if known_thy name then f name else ();
 
 fun get_thy name =
   (case lookup_thy name of
@@ -140,17 +128,11 @@
 val lookup_deps = Option.map #1 o lookup_thy;
 val get_deps = #1 o get_thy;
 fun change_deps name f = change_thy name (fn (deps, x) => (f deps, x));
+fun put_theory name theory = change_thy name (fn (deps, _) => (deps, SOME theory));
 
 val is_finished = is_none o get_deps;
 val master_directory = master_dir' o get_deps;
 
-fun loaded_files name =
-  (case get_deps name of
-    NONE => []
-  | SOME {master, files, ...} =>
-      (case master of SOME (thy_path, _) => [thy_path] | NONE => []) @
-      (map_filter (Option.map #1 o #2) files));
-
 fun get_parents name =
   thy_graph Graph.imm_preds name handle Graph.UNDEF _ =>
     error (loader_msg "nothing known about theory" [name]);
@@ -168,27 +150,18 @@
     SOME theory => theory
   | _ => error (loader_msg "undefined theory entry for" [name]));
 
+fun loaded_files name =
+  (case get_deps name of
+    NONE => []
+  | SOME {master, ...} =>
+      (case master of
+        NONE => []
+      | SOME (thy_path, _) => thy_path :: Thy_Load.loaded_files (get_theory name)));
+
 
 
 (** thy operations **)
 
-(* check state *)
-
-fun check_unfinished fail name =
-  if known_thy name andalso is_finished name then
-    fail (loader_msg "cannot update finished theory" [name])
-  else ();
-
-fun check_files name =
-  let
-    val files = (case get_deps name of SOME {files, ...} => files | NONE => []);
-    val missing_files = map_filter (fn (path, NONE) => SOME (Path.implode path) | _ => NONE) files;
-    val _ = null missing_files orelse
-      error (loader_msg "unresolved dependencies of theory" [name] ^
-        " on file(s): " ^ commas_quote missing_files);
-  in () end;
-
-
 (* maintain update_time *)
 
 local
@@ -207,14 +180,13 @@
 fun outdate_thy name =
   if is_finished name orelse is_outdated name then ()
   else CRITICAL (fn () =>
-   (change_deps name (Option.map (fn {master, text, parents, files, ...} =>
-    make_deps ~1 master text parents files)); perform Outdate name));
+   (change_deps name (Option.map (fn {master, text, parents, ...} =>
+    make_deps ~1 master text parents)); perform Outdate name));
 
 fun touch_thys names =
   List.app outdate_thy (thy_graph Graph.all_succs (map_filter unfinished names));
 
 fun touch_thy name = touch_thys [name];
-fun touch_child_thys name = touch_thys (thy_graph Graph.imm_succs name);
 
 end;
 
@@ -266,52 +238,6 @@
 val kill_thy = if_known_thy remove_thy;
 
 
-(* load_file *)
-
-local
-
-fun provide path name info (SOME {update_time, master, text, parents, files}) =
-     (if AList.defined (op =) files path then ()
-      else warning (loader_msg "undeclared dependency of theory" [name] ^
-        " on file: " ^ quote (Path.implode path));
-      SOME (make_deps update_time master text parents
-        (AList.update (op =) (path, SOME info) files)))
-  | provide _ _ _ NONE = NONE;
-
-fun run_file path =
-  (case Option.map (Context.theory_name o Context.the_theory) (Context.thread_data ()) of
-    NONE => (Thy_Load.load_ml Path.current path; ())
-  | SOME name =>
-      (case lookup_deps name of
-        SOME deps =>
-          change_deps name (provide path name (Thy_Load.load_ml (master_dir' deps) path))
-      | NONE => (Thy_Load.load_ml Path.current path; ())));
-
-in
-
-fun provide_file path name =
-  let
-    val dir = master_directory name;
-    val _ = check_unfinished error name;
-  in change_deps name (provide path name (Thy_Load.check_file dir path)) end;
-
-fun load_file path =
-  if ! Output.timing then
-    let val name = Path.implode path in
-      timeit (fn () =>
-       (priority ("\n**** Starting file " ^ quote name ^ " ****");
-        run_file path;
-        priority ("**** Finished file " ^ quote name ^ " ****\n")))
-    end
-  else run_file path;
-
-fun exec_file path = ML_Context.exec (fn () => load_file path);
-
-val use = load_file o Path.explode;
-
-end;
-
-
 (* load_thy *)
 
 fun required_by _ [] = ""
@@ -321,22 +247,23 @@
   let
     val _ = priority ("Loading theory " ^ quote name ^ required_by " " initiators);
     fun corrupted () = error (loader_msg "corrupted dependency information" [name]);
-    val (pos, text, _) =
+    val (pos, text) =
       (case get_deps name of
-        SOME {master = SOME (master_path, _), text, files, ...} =>
+        SOME {master = SOME (master_path, _), text, ...} =>
           if text = "" then corrupted ()
-          else (Path.position master_path, text, files)
+          else (Path.position master_path, text)
       | _ => corrupted ());
     val _ = touch_thy name;
-    val _ = CRITICAL (fn () =>
-      change_deps name (Option.map (fn {master, text, parents, files, ...} =>
-        make_deps upd_time master text parents files)));
-    val after_load = Outer_Syntax.load_thy name pos text;
+    val _ =
+      change_deps name (Option.map (fn {master, text, parents, ...} =>
+        make_deps upd_time master text parents));
+    val (after_load, theory) = Outer_Syntax.load_thy name pos text;
+    val _ = put_theory name theory;
     val _ =
       CRITICAL (fn () =>
        (change_deps name
-          (Option.map (fn {update_time, master, parents, files, ...} =>
-            make_deps update_time master "" parents files));
+          (Option.map (fn {update_time, master, parents, ...} =>
+            make_deps update_time master "" parents));
         perform Update name));
   in after_load end;
 
@@ -410,43 +337,33 @@
 
 local
 
-fun check_file master (src_path, info) =
-  let val info' =
-    (case info of
-      NONE => NONE
-    | SOME (_, id) =>
-        (case Thy_Load.test_file (master_dir master) src_path of
-          NONE => NONE
-        | SOME (path', id') => if id <> id' then NONE else SOME (path', id')))
-  in (src_path, info') end;
-
 fun check_deps dir name =
   (case lookup_deps name of
     SOME NONE => (true, NONE, get_parents name)
   | NONE =>
-      let val {master, text, imports = parents, uses = files} = Thy_Load.deps_thy dir name
-      in (false, init_deps (SOME master) text parents files, parents) end
-  | SOME (SOME {update_time, master, text, parents, files}) =>
+      let val {master, text, imports = parents, ...} = Thy_Load.deps_thy dir name
+      in (false, init_deps (SOME master) text parents, parents) end
+  | SOME (SOME {update_time, master, text, parents}) =>
       let
         val (thy_path, thy_id) = Thy_Load.check_thy dir name;
         val master' = SOME (thy_path, thy_id);
       in
         if Option.map #2 master <> SOME thy_id then
-          let val {text = text', imports = parents', uses = files', ...} =
-            Thy_Load.deps_thy dir name;
-          in (false, init_deps master' text' parents' files', parents') end
+          let val {text = text', imports = parents', ...} = Thy_Load.deps_thy dir name;
+          in (false, init_deps master' text' parents', parents') end
         else
           let
-            val files' = map (check_file master') files;
-            val current = update_time >= 0 andalso can get_theory name
-              andalso forall (is_some o snd) files';
+            val current =
+              (case lookup_theory name of
+                NONE => false
+              | SOME theory => update_time >= 0 andalso Thy_Load.all_current theory);
             val update_time' = if current then update_time else ~1;
-            val deps' = SOME (make_deps update_time' master' text parents files');
+            val deps' = SOME (make_deps update_time' master' text parents);
           in (current, deps', parents) end
       end);
 
-fun read_text (SOME {update_time, master = master as SOME (path, _), text = _, parents, files}) =
-  SOME (make_deps update_time master (File.read path) parents files);
+fun read_text (SOME {update_time, master = master as SOME (path, _), text = _, parents}) =
+  SOME (make_deps update_time master (File.read path) parents);
 
 in
 
@@ -495,28 +412,31 @@
   schedule_tasks (snd (require_thys [] dir arg Graph.empty));
 
 val use_thys = use_thys_dir Path.current;
-
-fun use_thy str =
-  let
-    val name = base_name str;
-    val _ = check_unfinished warning name;
-  in use_thys [str] end;
+val use_thy = use_thys o single;
 
 
-(* begin / end theory *)
+(* begin theory *)
+
+fun check_unfinished name =
+  if known_thy name andalso is_finished name then
+    error (loader_msg "cannot update finished theory" [name])
+  else ();
 
 fun begin_theory name parents uses int =
   let
     val parent_names = map base_name parents;
     val dir = master_dir'' (lookup_deps name);
-    val _ = check_unfinished error name;
+    val _ = check_unfinished name;
     val _ = if int then use_thys_dir dir parents else ();
 
-    val theory = Theory.begin_theory name (map get_theory parent_names);
+    val theory =
+      Theory.begin_theory name (map get_theory parent_names)
+      |> Thy_Load.init dir
+      |> fold (Thy_Load.require o fst) uses;
 
     val deps =
       if known_thy name then get_deps name
-      else init_deps NONE "" parents (map #1 uses);
+      else init_deps NONE "" parents;
     val _ = change_thys (new_deps name parent_names (deps, NONE));
 
     val update_time = (case deps of NONE => 0 | SOME {update_time, ...} => update_time);
@@ -527,59 +447,34 @@
 
     val uses_now = map_filter (fn (x, true) => SOME x | _ => NONE) uses;
     val theory'' =
-      fold (fn x => Context.theory_map (exec_file x) o Theory.checkpoint) uses_now theory';
+      fold (fn x => Context.theory_map (Thy_Load.exec_ml x) o Theory.checkpoint) uses_now theory';
   in theory'' end;
 
-fun end_theory theory =
-  let
-    val name = Context.theory_name theory;
-    val _ = check_files name;
-    val theory' = Theory.end_theory theory;
-    val _ = change_thy name (fn (deps, _) => (deps, SOME theory'));
-  in () end;
-
 
 (* register existing theories *)
 
-fun register_thy name =
-  let
-    val _ = priority ("Registering theory " ^ quote name);
-    val thy = get_theory name;
-    val _ = map get_theory (get_parents name);
-    val _ = check_unfinished error name;
-    val _ = touch_thy name;
-    val master = #master (Thy_Load.deps_thy Path.current name);
-    val upd_time = #2 (Management_Data.get thy);
-  in
-    CRITICAL (fn () =>
-     (change_deps name (Option.map
-       (fn {parents, files, ...} => make_deps upd_time (SOME master) "" parents files));
-      perform Update name))
-  end;
-
-fun register_theory theory =
+fun register_thy theory =
   let
     val name = Context.theory_name theory;
-    val parents = Theory.parents_of theory;
-    val parent_names = map Context.theory_name parents;
-
-    fun err txt bads =
-      error (loader_msg txt bads ^ "\ncannot register theory " ^ quote name);
+    val _ = priority ("Registering theory " ^ quote name);
+    val parent_names = map Context.theory_name (Theory.parents_of theory);
+    val _ = map get_theory parent_names;
 
-    val nonfinished = filter_out is_finished parent_names;
-    fun get_variant (x, y_name) =
-      if Theory.eq_thy (x, get_theory y_name) then NONE
-      else SOME y_name;
-    val variants = map_filter get_variant (parents ~~ parent_names);
-
-    fun register G =
-      (Graph.new_node (name, (NONE, SOME theory)) G
-        handle Graph.DUP _ => err "duplicate theory entry" [])
-      |> add_deps name parent_names;
+    val master = Thy_Load.check_thy (Thy_Load.master_directory theory) name;
+    val update_time = #2 (Management_Data.get theory);
+    val parents =
+      (case lookup_deps name of
+        SOME (SOME {parents, ...}) => parents
+      | _ => parent_names);
+    val deps = make_deps update_time (SOME master) "" parents;
   in
-    if not (null nonfinished) then err "non-finished parent theories" nonfinished
-    else if not (null variants) then err "different versions of parent theories" variants
-    else CRITICAL (fn () => (change_thys register; perform Update name))
+    CRITICAL (fn () =>
+     (if known_thy name then
+        (List.app remove_thy (thy_graph Graph.imm_succs name);
+          change_thys (Graph.del_nodes [name]))
+      else ();
+      change_thys (new_deps name parents (SOME deps, SOME theory));
+      perform Update name))
   end;
 
 
diff -r d9549f9da779 -r a79abb22ca9c src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/Pure/Thy/thy_load.ML	Mon Jul 26 18:25:19 2010 +0200
@@ -17,21 +17,65 @@
 signature THY_LOAD =
 sig
   include BASIC_THY_LOAD
-  val ml_path: string -> Path.T
-  val thy_path: string -> Path.T
-  val split_thy_path: Path.T -> Path.T * string
-  val consistent_name: string -> string -> unit
+  val master_directory: theory -> Path.T
+  val init: Path.T -> theory -> theory
+  val require: Path.T -> theory -> theory
+  val provide: Path.T * (Path.T * File.ident) -> theory -> theory
   val test_file: Path.T -> Path.T -> (Path.T * File.ident) option
   val check_file: Path.T -> Path.T -> Path.T * File.ident
   val check_thy: Path.T -> string -> Path.T * File.ident
   val deps_thy: Path.T -> string ->
    {master: Path.T * File.ident, text: string, imports: string list, uses: Path.T list}
-  val load_ml: Path.T -> Path.T -> Path.T * File.ident
+  val loaded_files: theory -> Path.T list
+  val all_current: theory -> bool
+  val provide_file: Path.T -> theory -> theory
+  val use_ml: Path.T -> unit
+  val exec_ml: Path.T -> generic_theory -> generic_theory
 end;
 
 structure Thy_Load: THY_LOAD =
 struct
 
+(* manage source files *)
+
+type files =
+ {master_dir: Path.T,                                 (*master directory of theory source*)
+  required: Path.T list,                              (*source path*)
+  provided: (Path.T * (Path.T * File.ident)) list};   (*source path, physical path, identifier*)
+
+fun make_files (master_dir, required, provided): files =
+ {master_dir = master_dir, required = required, provided = provided};
+
+structure Files = Theory_Data
+(
+  type T = files;
+  val empty = make_files (Path.current, [], []);
+  fun extend _ = empty;
+  fun merge _ = empty;
+);
+
+fun map_files f =
+  Files.map (fn {master_dir, required, provided} =>
+    make_files (f (master_dir, required, provided)));
+
+
+val master_directory = #master_dir o Files.get;
+
+fun init master_dir = map_files (fn _ => (master_dir, [], []));
+
+fun require src_path =
+  map_files (fn (master_dir, required, provided) =>
+    if member (op =) required src_path then
+      error ("Duplicate source file dependency: " ^ Path.implode src_path)
+    else (master_dir, src_path :: required, provided));
+
+fun provide (src_path, path_info) =
+  map_files (fn (master_dir, required, provided) =>
+    if AList.defined (op =) provided src_path then
+      error ("Duplicate resolution of source file dependency: " ^ Path.implode src_path)
+    else (master_dir, required, (src_path, path_info) :: provided));
+
+
 (* maintain load path *)
 
 local val load_path = Unsynchronized.ref [Path.current] in
@@ -56,22 +100,6 @@
 end;
 
 
-(* file formats *)
-
-val ml_path = Path.ext "ML" o Path.basic;
-val thy_path = Path.ext "thy" o Path.basic;
-
-fun split_thy_path path =
-  (case Path.split_ext path of
-    (path', "thy") => (Path.dir path', Path.implode (Path.base path'))
-  | _ => error ("Bad theory file specification " ^ Path.implode path));
-
-fun consistent_name name name' =
-  if name = name' then ()
-  else error ("Filename " ^ quote (Path.implode (thy_path name)) ^
-    " does not agree with theory name " ^ quote name');
-
-
 (* check files *)
 
 local
@@ -103,7 +131,7 @@
     error ("Could not find file " ^ quote (Path.implode path) ^
       "\nin " ^ commas_quote (map Path.implode prfxs));
 
-fun check_thy dir name = check_file dir (thy_path name);
+fun check_thy dir name = check_file dir (Thy_Header.thy_path name);
 
 end;
 
@@ -116,18 +144,63 @@
     val text = File.read path;
     val (name', imports, uses) =
       Thy_Header.read (Path.position path) (Source.of_string_limited 8000 text);
-    val _ = consistent_name name name';
+    val _ = Thy_Header.consistent_name name name';
     val uses = map (Path.explode o #1) uses;
   in {master = master, text = text, imports = imports, uses = uses} end;
 
 
-(* ML files *)
+
+(* loaded files *)
+
+val loaded_files = map (#1 o #2) o #provided o Files.get;
 
-fun load_ml dir raw_path =
+fun check_loaded thy =
+  let
+    val {required, provided, ...} = Files.get thy;
+    val provided_paths = map #1 provided;
+    val _ =
+      (case subtract (op =) provided_paths required of
+        [] => NONE
+      | bad => error ("Pending source file dependencies: " ^ commas (map Path.implode (rev bad))));
+    val _ =
+      (case subtract (op =) required provided_paths of
+        [] => NONE
+      | bad => error ("Undeclared source file dependencies: " ^ commas (map Path.implode (rev bad))));
+  in () end;
+
+fun all_current thy =
   let
-    val (path, id) = check_file dir raw_path;
-    val _ = ML_Context.eval_file path;
-  in (path, id) end;
+    val {master_dir, provided, ...} = Files.get thy;
+    fun current (src_path, path_info) =
+      (case test_file master_dir src_path of
+        NONE => false
+      | SOME path_info' => eq_snd (op =) (path_info, path_info'));
+  in can check_loaded thy andalso forall current provided end;
+
+val _ = Context.>> (Context.map_theory (Theory.at_end (fn thy => (check_loaded thy; NONE))));
+
+
+(* provide files *)
+
+fun provide_file src_path thy =
+  provide (src_path, check_file (master_directory thy) src_path) thy;
+
+fun use_ml src_path =
+  if is_none (Context.thread_data ()) then
+    ML_Context.eval_file (#1 (check_file Path.current src_path))
+  else
+    let
+      val thy = ML_Context.the_global_context ();
+      val (path, info) = check_file (master_directory thy) src_path;
+
+      val _ = ML_Context.eval_file path;
+      val _ = Context.>> Local_Theory.propagate_ml_env;
+
+      val provide = provide (src_path, (path, info));
+      val _ = Context.>> (Context.mapping provide (Local_Theory.theory provide));
+    in () end
+
+fun exec_ml src_path = ML_Context.exec (fn () => use_ml src_path);
 
 end;
 
diff -r d9549f9da779 -r a79abb22ca9c src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/Pure/pure_setup.ML	Mon Jul 26 18:25:19 2010 +0200
@@ -4,14 +4,16 @@
 Pure theory and ML toplevel setup.
 *)
 
-(* the Pure theories *)
+(* the Pure theory *)
 
 Context.>> (Context.map_theory
  (Outer_Syntax.process_file (Path.explode "Pure.thy") #>
   Theory.end_theory));
+
 structure Pure = struct val thy = ML_Context.the_global_context () end;
+
 Context.set_thread_data NONE;
-Thy_Info.register_theory Pure.thy;
+Thy_Info.register_thy Pure.thy;
 
 
 (* ML toplevel pretty printing *)
@@ -51,7 +53,8 @@
 
 (* ML toplevel use commands *)
 
-fun use name = Toplevel.program (fn () => Thy_Info.use name);
+fun use name = Toplevel.program (fn () => Thy_Load.use_ml (Path.explode name));
+
 fun use_thys name = Toplevel.program (fn () => Thy_Info.use_thys name);
 fun use_thy name = Toplevel.program (fn () => Thy_Info.use_thy name);
 
diff -r d9549f9da779 -r a79abb22ca9c src/Tools/Code/code_eval.ML
--- a/src/Tools/Code/code_eval.ML	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/Tools/Code/code_eval.ML	Mon Jul 26 18:25:19 2010 +0200
@@ -173,7 +173,8 @@
       end
   | process (code_body, _) _ (SOME file_name) thy =
       let
-        val preamble = "(* Generated from " ^ Path.implode (Thy_Load.thy_path (Context.theory_name thy))
+        val preamble =
+          "(* Generated from " ^ Path.implode (Thy_Header.thy_path (Context.theory_name thy))
           ^ "; DO NOT EDIT! *)";
         val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code_body);
       in