avoid internal names;
authorwenzelm
Sun Sep 30 21:55:15 2007 +0200 (2007-09-30)
changeset 247835a3e336a2e37
parent 24782 38e5c05ef741
child 24784 102e0e732495
avoid internal names;
src/Cube/Cube.thy
src/HOL/Bali/AxCompl.thy
src/HOL/Bali/AxSem.thy
src/HOL/Bali/Conform.thy
src/HOL/Bali/Decl.thy
src/HOL/Bali/DefiniteAssignmentCorrect.thy
src/HOL/Bali/Name.thy
src/HOL/Bali/Term.thy
src/HOL/Bali/TypeRel.thy
src/HOL/Bali/TypeSafe.thy
src/HOL/Bali/WellType.thy
src/HOL/Complex/ex/ReflectedFerrack.thy
src/HOL/MetisExamples/Abstraction.thy
src/HOL/MicroJava/J/Conform.thy
src/HOL/MicroJava/J/Example.thy
src/HOL/MicroJava/J/JBasis.thy
src/HOL/MicroJava/J/JListExample.thy
src/HOL/MicroJava/J/State.thy
src/HOL/MicroJava/J/Value.thy
src/HOL/MicroJava/JVM/JVMListExample.thy
src/ZF/AC/WO6_WO1.thy
     1.1 --- a/src/Cube/Cube.thy	Sun Sep 30 16:53:08 2007 +0200
     1.2 +++ b/src/Cube/Cube.thy	Sun Sep 30 21:55:15 2007 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4  typedecl typing
     1.5  
     1.6  nonterminals
     1.7 -  context_ typing_
     1.8 +  context' typing'
     1.9  
    1.10  consts
    1.11    Abs           :: "[term, term => term] => term"
    1.12 @@ -28,13 +28,13 @@
    1.13    Has_type      :: "[term, term] => typing"
    1.14  
    1.15  syntax
    1.16 -  Trueprop      :: "[context_, typing_] => prop"        ("(_/ |- _)")
    1.17 -  Trueprop1     :: "typing_ => prop"                    ("(_)")
    1.18 -  ""            :: "id => context_"                     ("_")
    1.19 -  ""            :: "var => context_"                    ("_")
    1.20 -  MT_context    :: "context_"                           ("")
    1.21 -  Context       :: "[typing_, context_] => context_"    ("_ _")
    1.22 -  Has_type      :: "[term, term] => typing_"            ("(_:/ _)" [0, 0] 5)
    1.23 +  Trueprop      :: "[context', typing'] => prop"        ("(_/ |- _)")
    1.24 +  Trueprop1     :: "typing' => prop"                    ("(_)")
    1.25 +  ""            :: "id => context'"                     ("_")
    1.26 +  ""            :: "var => context'"                    ("_")
    1.27 +  MT_context    :: "context'"                           ("")
    1.28 +  Context       :: "[typing', context'] => context'"    ("_ _")
    1.29 +  Has_type      :: "[term, term] => typing'"            ("(_:/ _)" [0, 0] 5)
    1.30    Lam           :: "[idt, term, term] => term"          ("(3Lam _:_./ _)" [0, 0, 0] 10)
    1.31    Pi            :: "[idt, term, term] => term"          ("(3Pi _:_./ _)" [0, 0] 10)
    1.32    arrow         :: "[term, term] => term"               (infixr "->" 10)
    1.33 @@ -46,7 +46,7 @@
    1.34    "A -> B"       => "Prod(A, %_. B)"
    1.35  
    1.36  syntax (xsymbols)
    1.37 -  Trueprop      :: "[context_, typing_] => prop"        ("(_/ \<turnstile> _)")
    1.38 +  Trueprop      :: "[context', typing'] => prop"        ("(_/ \<turnstile> _)")
    1.39    box           :: "term"                               ("\<box>")
    1.40    Lam           :: "[idt, term, term] => term"          ("(3\<Lambda> _:_./ _)" [0, 0, 0] 10)
    1.41    Pi            :: "[idt, term, term] => term"          ("(3\<Pi> _:_./ _)" [0, 0] 10)
     2.1 --- a/src/HOL/Bali/AxCompl.thy	Sun Sep 30 16:53:08 2007 +0200
     2.2 +++ b/src/HOL/Bali/AxCompl.thy	Sun Sep 30 21:55:15 2007 +0200
     2.3 @@ -1277,7 +1277,7 @@
     2.4  	apply (fastsimp intro: eval.Comp) 
     2.5  	done
     2.6      next
     2.7 -      case (If_ e c1 c2)
     2.8 +      case (If' e c1 c2)
     2.9        thus "G,A\<turnstile>{=:n} \<langle>If(e) c1 Else c2\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
    2.10  	apply -
    2.11  	apply (rule MGFn_NormalI)
     3.1 --- a/src/HOL/Bali/AxSem.thy	Sun Sep 30 16:53:08 2007 +0200
     3.2 +++ b/src/HOL/Bali/AxSem.thy	Sun Sep 30 21:55:15 2007 +0200
     3.3 @@ -49,9 +49,9 @@
     3.4    "Vals x"     => "(In3 x)"
     3.5  
     3.6  syntax
     3.7 -  "Val_"    :: "[pttrn] => pttrn"     ("Val:_"  [951] 950)
     3.8 -  "Var_"    :: "[pttrn] => pttrn"     ("Var:_"  [951] 950)
     3.9 -  "Vals_"   :: "[pttrn] => pttrn"     ("Vals:_" [951] 950)
    3.10 +  "_Val"    :: "[pttrn] => pttrn"     ("Val:_"  [951] 950)
    3.11 +  "_Var"    :: "[pttrn] => pttrn"     ("Var:_"  [951] 950)
    3.12 +  "_Vals"   :: "[pttrn] => pttrn"     ("Vals:_" [951] 950)
    3.13  
    3.14  translations
    3.15    "\<lambda>Val:v . b"  == "(\<lambda>v. b) \<circ> the_In1"
     4.1 --- a/src/HOL/Bali/Conform.thy	Sun Sep 30 16:53:08 2007 +0200
     4.2 +++ b/src/HOL/Bali/Conform.thy	Sun Sep 30 21:55:15 2007 +0200
     4.3 @@ -17,7 +17,7 @@
     4.4  \end{itemize}
     4.5  *}
     4.6  
     4.7 -types	env_ = "prog \<times> (lname, ty) table" (* same as env of WellType.thy *)
     4.8 +types	env' = "prog \<times> (lname, ty) table" (* same as env of WellType.thy *)
     4.9  
    4.10  
    4.11  section "extension of global store"
    4.12 @@ -388,7 +388,7 @@
    4.13  
    4.14  constdefs
    4.15  
    4.16 -  conforms :: "state \<Rightarrow> env_ \<Rightarrow> bool"          (     "_\<Colon>\<preceq>_"   [71,71]      70)
    4.17 +  conforms :: "state \<Rightarrow> env' \<Rightarrow> bool"          (     "_\<Colon>\<preceq>_"   [71,71]      70)
    4.18     "xs\<Colon>\<preceq>E \<equiv> let (G, L) = E; s = snd xs; l = locals s in
    4.19      (\<forall>r. \<forall>obj\<in>globs s r:           G,s\<turnstile>obj   \<Colon>\<preceq>\<surd>r) \<and>
    4.20                  \<spacespace>                   G,s\<turnstile>l    [\<sim>\<Colon>\<preceq>]L\<spacespace> \<and>
     5.1 --- a/src/HOL/Bali/Decl.thy	Sun Sep 30 16:53:08 2007 +0200
     5.2 +++ b/src/HOL/Bali/Decl.thy	Sun Sep 30 21:55:15 2007 +0200
     5.3 @@ -447,14 +447,14 @@
     5.4    subcls1_def: "subcls1 G \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c\<in>class G C: super c = D)}"
     5.5  
     5.6  syntax
     5.7 - "@subcls1" :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70)
     5.8 - "@subclseq":: "prog => [qtname, qtname] => bool" ("_|-_<=:C _"[71,71,71] 70)
     5.9 - "@subcls"  :: "prog => [qtname, qtname] => bool" ("_|-_<:C _"[71,71,71] 70)
    5.10 + "_subcls1" :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70)
    5.11 + "_subclseq":: "prog => [qtname, qtname] => bool" ("_|-_<=:C _"[71,71,71] 70)
    5.12 + "_subcls"  :: "prog => [qtname, qtname] => bool" ("_|-_<:C _"[71,71,71] 70)
    5.13  
    5.14  syntax (xsymbols)
    5.15 -  "@subcls1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C\<^sub>1_"  [71,71,71] 70)
    5.16 -  "@subclseq":: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>\<^sub>C _"  [71,71,71] 70)
    5.17 -  "@subcls"  :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C _"  [71,71,71] 70)
    5.18 +  "_subcls1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C\<^sub>1_"  [71,71,71] 70)
    5.19 +  "_subclseq":: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>\<^sub>C _"  [71,71,71] 70)
    5.20 +  "_subcls"  :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C _"  [71,71,71] 70)
    5.21  
    5.22  translations
    5.23          "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D" == "(C,D) \<in> subcls1 G"
     6.1 --- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Sun Sep 30 16:53:08 2007 +0200
     6.2 +++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Sun Sep 30 21:55:15 2007 +0200
     6.3 @@ -129,11 +129,11 @@
     6.4      ultimately show ?case
     6.5        by simp
     6.6    next
     6.7 -    case (If_ e c1 c2 jmps' jmps)
     6.8 -    from If_.prems 
     6.9 -    have "jumpNestingOkS jmps c1" by - (rule If_.hyps,auto)
    6.10 -    moreover from If_.prems 
    6.11 -    have "jumpNestingOkS jmps c2" by - (rule If_.hyps,auto)
    6.12 +    case (If' e c1 c2 jmps' jmps)
    6.13 +    from If'.prems 
    6.14 +    have "jumpNestingOkS jmps c1" by - (rule If'.hyps,auto)
    6.15 +    moreover from If'.prems 
    6.16 +    have "jumpNestingOkS jmps c2" by - (rule If'.hyps,auto)
    6.17      ultimately show ?case
    6.18        by simp
    6.19    next
     7.1 --- a/src/HOL/Bali/Name.thy	Sun Sep 30 16:53:08 2007 +0200
     7.2 +++ b/src/HOL/Bali/Name.thy	Sun Sep 30 21:55:15 2007 +0200
     7.3 @@ -43,8 +43,8 @@
     7.4  
     7.5  
     7.6  datatype tname	--{* type names for standard classes and other type names *}
     7.7 -	= Object_
     7.8 -	| SXcpt_   xname
     7.9 +	= Object'
    7.10 +	| SXcpt'   xname
    7.11  	| TName   tnam
    7.12  
    7.13  record   qtname = --{* qualified tname cf. 6.5.3, 6.5.4*}
    7.14 @@ -90,8 +90,8 @@
    7.15    Object :: qtname
    7.16    SXcpt  :: "xname \<Rightarrow> qtname"
    7.17  defs
    7.18 -  Object_def: "Object  \<equiv> \<lparr>pid = java_lang, tid = Object_\<rparr>"
    7.19 -  SXcpt_def:  "SXcpt   \<equiv> \<lambda>x.  \<lparr>pid = java_lang, tid = SXcpt_ x\<rparr>"
    7.20 +  Object_def: "Object  \<equiv> \<lparr>pid = java_lang, tid = Object'\<rparr>"
    7.21 +  SXcpt_def:  "SXcpt   \<equiv> \<lambda>x.  \<lparr>pid = java_lang, tid = SXcpt' x\<rparr>"
    7.22  
    7.23  lemma Object_neq_SXcpt [simp]: "Object \<noteq> SXcpt xn"
    7.24  by (simp add: Object_def SXcpt_def)
     8.1 --- a/src/HOL/Bali/Term.thy	Sun Sep 30 16:53:08 2007 +0200
     8.2 +++ b/src/HOL/Bali/Term.thy	Sun Sep 30 21:55:15 2007 +0200
     8.3 @@ -203,7 +203,7 @@
     8.4          | Lab   jump stmt       ("_\<bullet> _" [      99,66]66)
     8.5                                  --{* labeled statement; handles break *}
     8.6  	| Comp  stmt stmt       ("_;; _"                  [      66,65]65)
     8.7 -	| If_   expr stmt stmt  ("If'(_') _ Else _"       [   80,79,79]70)
     8.8 +	| If'   expr stmt stmt  ("If'(_') _ Else _"       [   80,79,79]70)
     8.9  	| Loop  label expr stmt ("_\<bullet> While'(_') _"        [   99,80,79]70)
    8.10          | Jmp jump              --{* break, continue, return *}
    8.11  	| Throw expr
     9.1 --- a/src/HOL/Bali/TypeRel.thy	Sun Sep 30 16:53:08 2007 +0200
     9.2 +++ b/src/HOL/Bali/TypeRel.thy	Sun Sep 30 21:55:15 2007 +0200
     9.3 @@ -37,25 +37,25 @@
     9.4  
     9.5  syntax
     9.6  
     9.7 - "@subint1" :: "prog => [qtname, qtname] => bool" ("_|-_<:I1_" [71,71,71] 70)
     9.8 - "@subint"  :: "prog => [qtname, qtname] => bool" ("_|-_<=:I _"[71,71,71] 70)
     9.9 + "_subint1" :: "prog => [qtname, qtname] => bool" ("_|-_<:I1_" [71,71,71] 70)
    9.10 + "_subint"  :: "prog => [qtname, qtname] => bool" ("_|-_<=:I _"[71,71,71] 70)
    9.11   (* Defined in Decl.thy:
    9.12 - "@subcls1" :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70)
    9.13 - "@subclseq":: "prog => [qtname, qtname] => bool" ("_|-_<=:C _"[71,71,71] 70)
    9.14 - "@subcls"  :: "prog => [qtname, qtname] => bool" ("_|-_<:C _"[71,71,71] 70)
    9.15 + "_subcls1" :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70)
    9.16 + "_subclseq":: "prog => [qtname, qtname] => bool" ("_|-_<=:C _"[71,71,71] 70)
    9.17 + "_subcls"  :: "prog => [qtname, qtname] => bool" ("_|-_<:C _"[71,71,71] 70)
    9.18   *)
    9.19   "@implmt1" :: "prog => [qtname, qtname] => bool" ("_|-_~>1_"  [71,71,71] 70)
    9.20  
    9.21  syntax (xsymbols)
    9.22  
    9.23 -  "@subint1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>I1_"  [71,71,71] 70)
    9.24 -  "@subint"  :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>I _"  [71,71,71] 70)
    9.25 +  "_subint1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>I1_"  [71,71,71] 70)
    9.26 +  "_subint"  :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>I _"  [71,71,71] 70)
    9.27    (* Defined in Decl.thy:
    9.28 -\  "@subcls1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C\<^sub>1_"  [71,71,71] 70)
    9.29 -  "@subclseq":: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>\<^sub>C _"  [71,71,71] 70)
    9.30 -  "@subcls"  :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C _"  [71,71,71] 70)
    9.31 +\  "_subcls1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C\<^sub>1_"  [71,71,71] 70)
    9.32 +  "_subclseq":: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>\<^sub>C _"  [71,71,71] 70)
    9.33 +  "_subcls"  :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C _"  [71,71,71] 70)
    9.34    *)
    9.35 -  "@implmt1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<leadsto>1_"  [71,71,71] 70)
    9.36 +  "_implmt1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<leadsto>1_"  [71,71,71] 70)
    9.37  
    9.38  translations
    9.39  
    10.1 --- a/src/HOL/Bali/TypeSafe.thy	Sun Sep 30 16:53:08 2007 +0200
    10.2 +++ b/src/HOL/Bali/TypeSafe.thy	Sun Sep 30 21:55:15 2007 +0200
    10.3 @@ -97,7 +97,7 @@
    10.4  section "result conformance"
    10.5  
    10.6  constdefs
    10.7 -  assign_conforms :: "st \<Rightarrow> (val \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> ty \<Rightarrow> env_ \<Rightarrow> bool"
    10.8 +  assign_conforms :: "st \<Rightarrow> (val \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> ty \<Rightarrow> env' \<Rightarrow> bool"
    10.9            ("_\<le>|_\<preceq>_\<Colon>\<preceq>_"                                        [71,71,71,71] 70)
   10.10  "s\<le>|f\<preceq>T\<Colon>\<preceq>E \<equiv>
   10.11   (\<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>
    11.1 --- a/src/HOL/Bali/WellType.thy	Sun Sep 30 16:53:08 2007 +0200
    11.2 +++ b/src/HOL/Bali/WellType.thy	Sun Sep 30 21:55:15 2007 +0200
    11.3 @@ -426,19 +426,19 @@
    11.4  
    11.5  
    11.6  syntax (* for purely static typing *)
    11.7 -  wt_      :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
    11.8 -  wt_stmt_ :: "env \<Rightarrow>  stmt       \<Rightarrow> bool" ("_|-_:<>" [51,51   ] 50)
    11.9 -  ty_expr_ :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50)
   11.10 -  ty_var_  :: "env \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50)
   11.11 -  ty_exprs_:: "env \<Rightarrow> [expr list,
   11.12 +  "_wt"      :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
   11.13 +  "_wt_stmt" :: "env \<Rightarrow>  stmt       \<Rightarrow> bool" ("_|-_:<>" [51,51   ] 50)
   11.14 +  "_ty_expr" :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50)
   11.15 +  "_ty_var"  :: "env \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50)
   11.16 +  "_ty_exprs":: "env \<Rightarrow> [expr list,
   11.17  		     \<spacespace> ty   list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50)
   11.18  
   11.19  syntax (xsymbols)
   11.20 -  wt_      :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>_"  [51,51,51] 50)
   11.21 -  wt_stmt_ ::  "env \<Rightarrow>  stmt       \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<surd>"  [51,51   ] 50)
   11.22 -  ty_expr_ :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>-_" [51,51,51] 50)
   11.23 -  ty_var_  :: "env \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>=_" [51,51,51] 50)
   11.24 -  ty_exprs_ :: "env \<Rightarrow> [expr list,
   11.25 +  "_wt"      :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>_"  [51,51,51] 50)
   11.26 +  "_wt_stmt" ::  "env \<Rightarrow>  stmt       \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<surd>"  [51,51   ] 50)
   11.27 +  "_ty_expr" :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>-_" [51,51,51] 50)
   11.28 +  "_ty_var"  :: "env \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>=_" [51,51,51] 50)
   11.29 +  "_ty_exprs" :: "env \<Rightarrow> [expr list,
   11.30  		    \<spacespace>  ty   list] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50)
   11.31  
   11.32  translations
    12.1 --- a/src/HOL/Complex/ex/ReflectedFerrack.thy	Sun Sep 30 16:53:08 2007 +0200
    12.2 +++ b/src/HOL/Complex/ex/ReflectedFerrack.thy	Sun Sep 30 21:55:15 2007 +0200
    12.3 @@ -1908,7 +1908,7 @@
    12.4    from alluopairs_set1[where xs="?U"] have UpU: "set ?Up \<le> (set ?U \<times> set ?U)" by simp
    12.5    from uset_l[OF lq] have U_l: "\<forall> (t,n) \<in> set ?U. numbound0 t \<and> n > 0" .
    12.6    from U_l UpU 
    12.7 -  have Up_: "\<forall> ((t,n),(s,m)) \<in> set ?Up. numbound0 t \<and> n> 0 \<and> numbound0 s \<and> m > 0" by auto
    12.8 +  have "\<forall> ((t,n),(s,m)) \<in> set ?Up. numbound0 t \<and> n> 0 \<and> numbound0 s \<and> m > 0" by auto
    12.9    hence Snb: "\<forall> (t,n) \<in> set ?S. numbound0 t \<and> n > 0 "
   12.10      by (auto simp add: mult_pos_pos)
   12.11    have Y_l: "\<forall> (t,n) \<in> set ?Y. numbound0 t \<and> n > 0" 
    13.1 --- a/src/HOL/MetisExamples/Abstraction.thy	Sun Sep 30 16:53:08 2007 +0200
    13.2 +++ b/src/HOL/MetisExamples/Abstraction.thy	Sun Sep 30 21:55:15 2007 +0200
    13.3 @@ -94,10 +94,10 @@
    13.4  proof (neg_clausify)
    13.5  assume 0: "\<And>cl\<Colon>'a\<Colon>type set.
    13.6     (llabs_subgoal_1\<Colon>'a\<Colon>type set \<Rightarrow> 'a\<Colon>type set) cl =
    13.7 -   Collect (llabs_Set_XCollect_ex_eq_3_ op \<in> (pset cl))"
    13.8 +   Collect (llabs_Set_XCollect_ex_eq_3 op \<in> (pset cl))"
    13.9  assume 1: "(f\<Colon>'a\<Colon>type) \<notin> pset (cl\<Colon>'a\<Colon>type set)"
   13.10  assume 2: "(cl\<Colon>'a\<Colon>type set, f\<Colon>'a\<Colon>type) \<in> (CLF\<Colon>('a\<Colon>type set \<times> 'a\<Colon>type) set)"
   13.11 -have 3: "llabs_Predicate_Xsup_Un_eq2_1_ (CLF\<Colon>('a\<Colon>type set \<times> 'a\<Colon>type) set)
   13.12 +have 3: "llabs_Predicate_Xsup_Un_eq2_1 (CLF\<Colon>('a\<Colon>type set \<times> 'a\<Colon>type) set)
   13.13   (cl\<Colon>'a\<Colon>type set) (f\<Colon>'a\<Colon>type)"
   13.14    by (metis acc_def 2)
   13.15  assume 4: "(CLF\<Colon>('a\<Colon>type set \<times> 'a\<Colon>type) set) =
   13.16 @@ -120,7 +120,7 @@
   13.17  assume 0: "\<And>cl\<Colon>'a\<Colon>type set.
   13.18     (llabs_subgoal_1\<Colon>'a\<Colon>type set \<Rightarrow> ('a\<Colon>type \<Rightarrow> 'a\<Colon>type) set) cl =
   13.19     Collect
   13.20 -    (llabs_Set_XCollect_ex_eq_3_ op \<in> (Pi (pset cl) (COMBK (pset cl))))"
   13.21 +    (llabs_Set_XCollect_ex_eq_3 op \<in> (Pi (pset cl) (COMBK (pset cl))))"
   13.22  assume 1: "(f\<Colon>'a\<Colon>type \<Rightarrow> 'a\<Colon>type) \<notin> Pi (pset (cl\<Colon>'a\<Colon>type set)) (COMBK (pset cl))"
   13.23  assume 2: "(cl\<Colon>'a\<Colon>type set, f\<Colon>'a\<Colon>type \<Rightarrow> 'a\<Colon>type)
   13.24  \<in> Sigma (CL\<Colon>'a\<Colon>type set set)
    14.1 --- a/src/HOL/MicroJava/J/Conform.thy	Sun Sep 30 16:53:08 2007 +0200
    14.2 +++ b/src/HOL/MicroJava/J/Conform.thy	Sun Sep 30 21:55:15 2007 +0200
    14.3 @@ -8,7 +8,7 @@
    14.4  
    14.5  theory Conform imports State WellType Exceptions begin
    14.6  
    14.7 -types 'c env_ = "'c prog \<times> (vname \<rightharpoonup> ty)"  -- "same as @{text env} of @{text WellType.thy}"
    14.8 +types 'c env' = "'c prog \<times> (vname \<rightharpoonup> ty)"  -- "same as @{text env} of @{text WellType.thy}"
    14.9  
   14.10  constdefs
   14.11  
   14.12 @@ -32,7 +32,7 @@
   14.13    xconf :: "aheap \<Rightarrow> val option \<Rightarrow> bool"
   14.14    "xconf hp vo  == preallocated hp \<and> (\<forall> v. (vo = Some v) \<longrightarrow> (\<exists> xc. v = (Addr (XcptRef xc))))"
   14.15  
   14.16 -  conforms :: "xstate => java_mb env_ => bool" ("_ ::<= _" [51,51] 50)
   14.17 +  conforms :: "xstate => java_mb env' => bool" ("_ ::<= _" [51,51] 50)
   14.18   "s::<=E == prg E|-h heap (store s) [ok] \<and> 
   14.19              prg E,heap (store s)|-locals (store s)[::<=]localT E \<and> 
   14.20              xconf (heap (store s)) (abrupt s)"
   14.21 @@ -54,7 +54,7 @@
   14.22    hconf    :: "'c prog => aheap => bool"
   14.23                ("_ \<turnstile>h _ \<surd>" [51,51] 50)
   14.24  
   14.25 -  conforms :: "state => java_mb env_ => bool"
   14.26 +  conforms :: "state => java_mb env' => bool"
   14.27                ("_ ::\<preceq> _" [51,51] 50)
   14.28  
   14.29  
    15.1 --- a/src/HOL/MicroJava/J/Example.thy	Sun Sep 30 16:53:08 2007 +0200
    15.2 +++ b/src/HOL/MicroJava/J/Example.thy	Sun Sep 30 21:55:15 2007 +0200
    15.3 @@ -37,23 +37,23 @@
    15.4  \end{verbatim}
    15.5  *}
    15.6  
    15.7 -datatype cnam_ = Base_ | Ext_
    15.8 -datatype vnam_ = vee_ | x_ | e_
    15.9 +datatype cnam' = Base' | Ext'
   15.10 +datatype vnam' = vee' | x' | e'
   15.11  
   15.12  consts
   15.13 -  cnam_ :: "cnam_ => cname"
   15.14 -  vnam_ :: "vnam_ => vnam"
   15.15 +  cnam' :: "cnam' => cname"
   15.16 +  vnam' :: "vnam' => vnam"
   15.17  
   15.18 --- "@{text cnam_} and @{text vnam_} are intended to be isomorphic 
   15.19 +-- "@{text cnam'} and @{text vnam'} are intended to be isomorphic 
   15.20      to @{text cnam} and @{text vnam}"
   15.21  axioms 
   15.22 -  inj_cnam_:  "(cnam_ x = cnam_ y) = (x = y)"
   15.23 -  inj_vnam_:  "(vnam_ x = vnam_ y) = (x = y)"
   15.24 +  inj_cnam':  "(cnam' x = cnam' y) = (x = y)"
   15.25 +  inj_vnam':  "(vnam' x = vnam' y) = (x = y)"
   15.26  
   15.27 -  surj_cnam_: "\<exists>m. n = cnam_ m"
   15.28 -  surj_vnam_: "\<exists>m. n = vnam_ m"
   15.29 +  surj_cnam': "\<exists>m. n = cnam' m"
   15.30 +  surj_vnam': "\<exists>m. n = vnam' m"
   15.31  
   15.32 -declare inj_cnam_ [simp] inj_vnam_ [simp]
   15.33 +declare inj_cnam' [simp] inj_vnam' [simp]
   15.34  
   15.35  syntax
   15.36    Base :: cname
   15.37 @@ -63,11 +63,11 @@
   15.38    e    :: vname
   15.39  
   15.40  translations
   15.41 -  "Base" == "cnam_ Base_"
   15.42 -  "Ext"  == "cnam_ Ext_"
   15.43 -  "vee"  == "VName (vnam_ vee_)"
   15.44 -  "x"  == "VName (vnam_ x_)"
   15.45 -  "e"  == "VName (vnam_ e_)"
   15.46 +  "Base" == "cnam' Base'"
   15.47 +  "Ext"  == "cnam' Ext'"
   15.48 +  "vee"  == "VName (vnam' vee')"
   15.49 +  "x"  == "VName (vnam' x')"
   15.50 +  "e"  == "VName (vnam' e')"
   15.51  
   15.52  axioms
   15.53    Base_not_Object: "Base \<noteq> Object"
   15.54 @@ -220,52 +220,52 @@
   15.55  
   15.56  declare ty_expr_ty_exprs_wt_stmt.intros [intro!]
   15.57  
   15.58 -lemma acyclic_subcls1_: "acyclicP (subcls1 tprg)"
   15.59 +lemma acyclic_subcls1': "acyclicP (subcls1 tprg)"
   15.60  apply (rule acyclicI [to_pred])
   15.61  apply safe
   15.62  done
   15.63  
   15.64 -lemmas wf_subcls1_ = acyclic_subcls1_ [THEN finite_subcls1 [THEN finite_acyclic_wf_converse [to_pred]]]
   15.65 +lemmas wf_subcls1' = acyclic_subcls1' [THEN finite_subcls1 [THEN finite_acyclic_wf_converse [to_pred]]]
   15.66  
   15.67 -lemmas fields_rec_ = wf_subcls1_ [THEN [2] fields_rec_lemma]
   15.68 +lemmas fields_rec' = wf_subcls1' [THEN [2] fields_rec_lemma]
   15.69  
   15.70  lemma fields_Object [simp]: "fields (tprg, Object) = []"
   15.71 -apply (subst fields_rec_)
   15.72 +apply (subst fields_rec')
   15.73  apply   auto
   15.74  done
   15.75  
   15.76  declare is_class_def [simp]
   15.77  
   15.78  lemma fields_Base [simp]: "fields (tprg,Base) = [((vee, Base), PrimT Boolean)]"
   15.79 -apply (subst fields_rec_)
   15.80 +apply (subst fields_rec')
   15.81  apply   auto
   15.82  done
   15.83  
   15.84  lemma fields_Ext [simp]: 
   15.85    "fields (tprg, Ext)  = [((vee, Ext ), PrimT Integer)] @ fields (tprg, Base)"
   15.86  apply (rule trans)
   15.87 -apply  (rule fields_rec_)
   15.88 +apply  (rule fields_rec')
   15.89  apply   auto
   15.90  done
   15.91  
   15.92 -lemmas method_rec_ = wf_subcls1_ [THEN [2] method_rec_lemma]
   15.93 +lemmas method_rec' = wf_subcls1' [THEN [2] method_rec_lemma]
   15.94  
   15.95  lemma method_Object [simp]: "method (tprg,Object) = map_of []"
   15.96 -apply (subst method_rec_)
   15.97 +apply (subst method_rec')
   15.98  apply  auto
   15.99  done
  15.100  
  15.101  lemma method_Base [simp]: "method (tprg, Base) = map_of  
  15.102    [((foo, [Class Base]), Base, (Class Base, foo_Base))]"
  15.103  apply (rule trans)
  15.104 -apply  (rule method_rec_)
  15.105 +apply  (rule method_rec')
  15.106  apply  auto
  15.107  done
  15.108  
  15.109  lemma method_Ext [simp]: "method (tprg, Ext) = (method (tprg, Base) ++ map_of  
  15.110    [((foo, [Class Base]), Ext , (Class Ext, foo_Ext))])"
  15.111  apply (rule trans)
  15.112 -apply  (rule method_rec_)
  15.113 +apply  (rule method_rec')
  15.114  apply  auto
  15.115  done
  15.116  
    16.1 --- a/src/HOL/MicroJava/J/JBasis.thy	Sun Sep 30 16:53:08 2007 +0200
    16.2 +++ b/src/HOL/MicroJava/J/JBasis.thy	Sun Sep 30 21:55:15 2007 +0200
    16.3 @@ -56,14 +56,14 @@
    16.4  apply  auto
    16.5  done
    16.6  
    16.7 -lemma Ball_set_table_: 
    16.8 +lemma Ball_set_table': 
    16.9    "(\<forall>(x,y)\<in>set l. P x y) --> (\<forall>x. \<forall>y. map_of l x = Some y --> P x y)"
   16.10  apply(induct_tac "l")
   16.11  apply(simp_all (no_asm))
   16.12  apply safe
   16.13  apply auto
   16.14  done
   16.15 -lemmas Ball_set_table = Ball_set_table_ [THEN mp];
   16.16 +lemmas Ball_set_table = Ball_set_table' [THEN mp];
   16.17  
   16.18  lemma table_of_remap_SomeD [rule_format (no_asm)]: 
   16.19  "map_of (map (\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) --> 
    17.1 --- a/src/HOL/MicroJava/J/JListExample.thy	Sun Sep 30 16:53:08 2007 +0200
    17.2 +++ b/src/HOL/MicroJava/J/JListExample.thy	Sun Sep 30 21:55:15 2007 +0200
    17.3 @@ -62,7 +62,7 @@
    17.4    cname ("string")
    17.5    vnam ("string")
    17.6    mname ("string")
    17.7 -  loc_ ("int")
    17.8 +  loc' ("int")
    17.9  
   17.10  consts_code
   17.11    "new_Addr" ("\<module>new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *} {* Loc *}")
    18.1 --- a/src/HOL/MicroJava/J/State.thy	Sun Sep 30 16:53:08 2007 +0200
    18.2 +++ b/src/HOL/MicroJava/J/State.thy	Sun Sep 30 21:55:15 2007 +0200
    18.3 @@ -9,9 +9,9 @@
    18.4  theory State imports TypeRel Value begin
    18.5  
    18.6  types 
    18.7 -  fields_ = "(vname \<times> cname \<rightharpoonup> val)"  -- "field name, defining class, value"
    18.8 +  fields' = "(vname \<times> cname \<rightharpoonup> val)"  -- "field name, defining class, value"
    18.9  
   18.10 -  obj = "cname \<times> fields_"    -- "class instance with class name and fields"
   18.11 +  obj = "cname \<times> fields'"    -- "class instance with class name and fields"
   18.12  
   18.13  constdefs
   18.14    obj_ty  :: "obj => ty"
    19.1 --- a/src/HOL/MicroJava/J/Value.thy	Sun Sep 30 16:53:08 2007 +0200
    19.2 +++ b/src/HOL/MicroJava/J/Value.thy	Sun Sep 30 21:55:15 2007 +0200
    19.3 @@ -8,11 +8,11 @@
    19.4  
    19.5  theory Value imports Type begin
    19.6  
    19.7 -typedecl loc_ -- "locations, i.e. abstract references on objects" 
    19.8 +typedecl loc' -- "locations, i.e. abstract references on objects" 
    19.9  
   19.10  datatype loc 
   19.11    = XcptRef xcpt -- "special locations for pre-allocated system exceptions"
   19.12 -  | Loc loc_     -- "usual locations (references on objects)"
   19.13 +  | Loc loc'     -- "usual locations (references on objects)"
   19.14  
   19.15  datatype val
   19.16    = Unit        -- "dummy result value of void methods"
    20.1 --- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Sun Sep 30 16:53:08 2007 +0200
    20.2 +++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Sun Sep 30 21:55:15 2007 +0200
    20.3 @@ -91,7 +91,7 @@
    20.4    cnam ("string")
    20.5    vnam ("string")
    20.6    mname ("string")
    20.7 -  loc_ ("int")
    20.8 +  loc' ("int")
    20.9  
   20.10  consts_code
   20.11    "new_Addr" ("\<module>new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}/ {* Loc *}")
    21.1 --- a/src/ZF/AC/WO6_WO1.thy	Sun Sep 30 16:53:08 2007 +0200
    21.2 +++ b/src/ZF/AC/WO6_WO1.thy	Sun Sep 30 21:55:15 2007 +0200
    21.3 @@ -75,13 +75,13 @@
    21.4  lemma lam_sets: "f \<in> A->B ==> (\<lambda>x \<in> A. {f`x}): A -> {{b}. b \<in> B}"
    21.5  by (fast intro!: lam_type apply_type)
    21.6  
    21.7 -lemma surj_imp_eq_: "f \<in> surj(A,B) ==> (\<Union>a \<in> A. {f`a}) = B"
    21.8 +lemma surj_imp_eq': "f \<in> surj(A,B) ==> (\<Union>a \<in> A. {f`a}) = B"
    21.9  apply (unfold surj_def)
   21.10  apply (fast elim!: apply_type)
   21.11  done
   21.12  
   21.13  lemma surj_imp_eq: "[| f \<in> surj(A,B); Ord(A) |] ==> (\<Union>a<A. {f`a}) = B"
   21.14 -by (fast dest!: surj_imp_eq_ intro!: ltI elim!: ltE)
   21.15 +by (fast dest!: surj_imp_eq' intro!: ltI elim!: ltE)
   21.16  
   21.17  lemma WO1_WO4: "WO1 ==> WO4(1)"
   21.18  apply (unfold WO1_def WO4_def)