--- a/src/Cube/Cube.thy Sun Sep 30 16:53:08 2007 +0200
+++ b/src/Cube/Cube.thy Sun Sep 30 21:55:15 2007 +0200
@@ -14,7 +14,7 @@
typedecl typing
nonterminals
- context_ typing_
+ context' typing'
consts
Abs :: "[term, term => term] => term"
@@ -28,13 +28,13 @@
Has_type :: "[term, term] => typing"
syntax
- Trueprop :: "[context_, typing_] => prop" ("(_/ |- _)")
- Trueprop1 :: "typing_ => prop" ("(_)")
- "" :: "id => context_" ("_")
- "" :: "var => context_" ("_")
- MT_context :: "context_" ("")
- Context :: "[typing_, context_] => context_" ("_ _")
- Has_type :: "[term, term] => typing_" ("(_:/ _)" [0, 0] 5)
+ Trueprop :: "[context', typing'] => prop" ("(_/ |- _)")
+ Trueprop1 :: "typing' => prop" ("(_)")
+ "" :: "id => context'" ("_")
+ "" :: "var => context'" ("_")
+ MT_context :: "context'" ("")
+ Context :: "[typing', context'] => context'" ("_ _")
+ Has_type :: "[term, term] => typing'" ("(_:/ _)" [0, 0] 5)
Lam :: "[idt, term, term] => term" ("(3Lam _:_./ _)" [0, 0, 0] 10)
Pi :: "[idt, term, term] => term" ("(3Pi _:_./ _)" [0, 0] 10)
arrow :: "[term, term] => term" (infixr "->" 10)
@@ -46,7 +46,7 @@
"A -> B" => "Prod(A, %_. B)"
syntax (xsymbols)
- Trueprop :: "[context_, typing_] => prop" ("(_/ \<turnstile> _)")
+ Trueprop :: "[context', typing'] => prop" ("(_/ \<turnstile> _)")
box :: "term" ("\<box>")
Lam :: "[idt, term, term] => term" ("(3\<Lambda> _:_./ _)" [0, 0, 0] 10)
Pi :: "[idt, term, term] => term" ("(3\<Pi> _:_./ _)" [0, 0] 10)
--- a/src/HOL/Bali/AxCompl.thy Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/Bali/AxCompl.thy Sun Sep 30 21:55:15 2007 +0200
@@ -1277,7 +1277,7 @@
apply (fastsimp intro: eval.Comp)
done
next
- case (If_ e c1 c2)
+ case (If' e c1 c2)
thus "G,A\<turnstile>{=:n} \<langle>If(e) c1 Else c2\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
apply -
apply (rule MGFn_NormalI)
--- a/src/HOL/Bali/AxSem.thy Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/Bali/AxSem.thy Sun Sep 30 21:55:15 2007 +0200
@@ -49,9 +49,9 @@
"Vals x" => "(In3 x)"
syntax
- "Val_" :: "[pttrn] => pttrn" ("Val:_" [951] 950)
- "Var_" :: "[pttrn] => pttrn" ("Var:_" [951] 950)
- "Vals_" :: "[pttrn] => pttrn" ("Vals:_" [951] 950)
+ "_Val" :: "[pttrn] => pttrn" ("Val:_" [951] 950)
+ "_Var" :: "[pttrn] => pttrn" ("Var:_" [951] 950)
+ "_Vals" :: "[pttrn] => pttrn" ("Vals:_" [951] 950)
translations
"\<lambda>Val:v . b" == "(\<lambda>v. b) \<circ> the_In1"
--- a/src/HOL/Bali/Conform.thy Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/Bali/Conform.thy Sun Sep 30 21:55:15 2007 +0200
@@ -17,7 +17,7 @@
\end{itemize}
*}
-types env_ = "prog \<times> (lname, ty) table" (* same as env of WellType.thy *)
+types env' = "prog \<times> (lname, ty) table" (* same as env of WellType.thy *)
section "extension of global store"
@@ -388,7 +388,7 @@
constdefs
- conforms :: "state \<Rightarrow> env_ \<Rightarrow> bool" ( "_\<Colon>\<preceq>_" [71,71] 70)
+ conforms :: "state \<Rightarrow> env' \<Rightarrow> bool" ( "_\<Colon>\<preceq>_" [71,71] 70)
"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>
--- a/src/HOL/Bali/Decl.thy Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/Bali/Decl.thy Sun Sep 30 21:55:15 2007 +0200
@@ -447,14 +447,14 @@
subcls1_def: "subcls1 G \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c\<in>class G C: super c = D)}"
syntax
- "@subcls1" :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70)
- "@subclseq":: "prog => [qtname, qtname] => bool" ("_|-_<=:C _"[71,71,71] 70)
- "@subcls" :: "prog => [qtname, qtname] => bool" ("_|-_<:C _"[71,71,71] 70)
+ "_subcls1" :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70)
+ "_subclseq":: "prog => [qtname, qtname] => bool" ("_|-_<=:C _"[71,71,71] 70)
+ "_subcls" :: "prog => [qtname, qtname] => bool" ("_|-_<:C _"[71,71,71] 70)
syntax (xsymbols)
- "@subcls1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C\<^sub>1_" [71,71,71] 70)
- "@subclseq":: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>\<^sub>C _" [71,71,71] 70)
- "@subcls" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C _" [71,71,71] 70)
+ "_subcls1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C\<^sub>1_" [71,71,71] 70)
+ "_subclseq":: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>\<^sub>C _" [71,71,71] 70)
+ "_subcls" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C _" [71,71,71] 70)
translations
"G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D" == "(C,D) \<in> subcls1 G"
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy Sun Sep 30 21:55:15 2007 +0200
@@ -129,11 +129,11 @@
ultimately show ?case
by simp
next
- case (If_ e c1 c2 jmps' jmps)
- from If_.prems
- have "jumpNestingOkS jmps c1" by - (rule If_.hyps,auto)
- moreover from If_.prems
- have "jumpNestingOkS jmps c2" by - (rule If_.hyps,auto)
+ case (If' e c1 c2 jmps' jmps)
+ from If'.prems
+ have "jumpNestingOkS jmps c1" by - (rule If'.hyps,auto)
+ moreover from If'.prems
+ have "jumpNestingOkS jmps c2" by - (rule If'.hyps,auto)
ultimately show ?case
by simp
next
--- a/src/HOL/Bali/Name.thy Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/Bali/Name.thy Sun Sep 30 21:55:15 2007 +0200
@@ -43,8 +43,8 @@
datatype tname --{* type names for standard classes and other type names *}
- = Object_
- | SXcpt_ xname
+ = Object'
+ | SXcpt' xname
| TName tnam
record qtname = --{* qualified tname cf. 6.5.3, 6.5.4*}
@@ -90,8 +90,8 @@
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>"
+ 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>"
lemma Object_neq_SXcpt [simp]: "Object \<noteq> SXcpt xn"
by (simp add: Object_def SXcpt_def)
--- a/src/HOL/Bali/Term.thy Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/Bali/Term.thy Sun Sep 30 21:55:15 2007 +0200
@@ -203,7 +203,7 @@
| Lab jump stmt ("_\<bullet> _" [ 99,66]66)
--{* labeled statement; handles break *}
| Comp stmt stmt ("_;; _" [ 66,65]65)
- | If_ expr stmt stmt ("If'(_') _ Else _" [ 80,79,79]70)
+ | If' expr stmt stmt ("If'(_') _ Else _" [ 80,79,79]70)
| Loop label expr stmt ("_\<bullet> While'(_') _" [ 99,80,79]70)
| Jmp jump --{* break, continue, return *}
| Throw expr
--- a/src/HOL/Bali/TypeRel.thy Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/Bali/TypeRel.thy Sun Sep 30 21:55:15 2007 +0200
@@ -37,25 +37,25 @@
syntax
- "@subint1" :: "prog => [qtname, qtname] => bool" ("_|-_<:I1_" [71,71,71] 70)
- "@subint" :: "prog => [qtname, qtname] => bool" ("_|-_<=:I _"[71,71,71] 70)
+ "_subint1" :: "prog => [qtname, qtname] => bool" ("_|-_<:I1_" [71,71,71] 70)
+ "_subint" :: "prog => [qtname, qtname] => bool" ("_|-_<=:I _"[71,71,71] 70)
(* Defined in Decl.thy:
- "@subcls1" :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70)
- "@subclseq":: "prog => [qtname, qtname] => bool" ("_|-_<=:C _"[71,71,71] 70)
- "@subcls" :: "prog => [qtname, qtname] => bool" ("_|-_<:C _"[71,71,71] 70)
+ "_subcls1" :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70)
+ "_subclseq":: "prog => [qtname, qtname] => bool" ("_|-_<=:C _"[71,71,71] 70)
+ "_subcls" :: "prog => [qtname, qtname] => bool" ("_|-_<:C _"[71,71,71] 70)
*)
"@implmt1" :: "prog => [qtname, qtname] => bool" ("_|-_~>1_" [71,71,71] 70)
syntax (xsymbols)
- "@subint1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>I1_" [71,71,71] 70)
- "@subint" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>I _" [71,71,71] 70)
+ "_subint1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>I1_" [71,71,71] 70)
+ "_subint" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>I _" [71,71,71] 70)
(* Defined in Decl.thy:
-\ "@subcls1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C\<^sub>1_" [71,71,71] 70)
- "@subclseq":: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>\<^sub>C _" [71,71,71] 70)
- "@subcls" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C _" [71,71,71] 70)
+\ "_subcls1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C\<^sub>1_" [71,71,71] 70)
+ "_subclseq":: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>\<^sub>C _" [71,71,71] 70)
+ "_subcls" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C _" [71,71,71] 70)
*)
- "@implmt1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<leadsto>1_" [71,71,71] 70)
+ "_implmt1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<leadsto>1_" [71,71,71] 70)
translations
--- a/src/HOL/Bali/TypeSafe.thy Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/Bali/TypeSafe.thy Sun Sep 30 21:55:15 2007 +0200
@@ -97,7 +97,7 @@
section "result conformance"
constdefs
- assign_conforms :: "st \<Rightarrow> (val \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> ty \<Rightarrow> env_ \<Rightarrow> bool"
+ assign_conforms :: "st \<Rightarrow> (val \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> ty \<Rightarrow> env' \<Rightarrow> bool"
("_\<le>|_\<preceq>_\<Colon>\<preceq>_" [71,71,71,71] 70)
"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>
--- a/src/HOL/Bali/WellType.thy Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/Bali/WellType.thy Sun Sep 30 21:55:15 2007 +0200
@@ -426,19 +426,19 @@
syntax (* for purely static typing *)
- wt_ :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
- wt_stmt_ :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_|-_:<>" [51,51 ] 50)
- ty_expr_ :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50)
- ty_var_ :: "env \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50)
- ty_exprs_:: "env \<Rightarrow> [expr list,
+ "_wt" :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
+ "_wt_stmt" :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_|-_:<>" [51,51 ] 50)
+ "_ty_expr" :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50)
+ "_ty_var" :: "env \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50)
+ "_ty_exprs":: "env \<Rightarrow> [expr list,
\<spacespace> ty list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50)
syntax (xsymbols)
- wt_ :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>_" [51,51,51] 50)
- wt_stmt_ :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<surd>" [51,51 ] 50)
- ty_expr_ :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>-_" [51,51,51] 50)
- ty_var_ :: "env \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>=_" [51,51,51] 50)
- ty_exprs_ :: "env \<Rightarrow> [expr list,
+ "_wt" :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>_" [51,51,51] 50)
+ "_wt_stmt" :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<surd>" [51,51 ] 50)
+ "_ty_expr" :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>-_" [51,51,51] 50)
+ "_ty_var" :: "env \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>=_" [51,51,51] 50)
+ "_ty_exprs" :: "env \<Rightarrow> [expr list,
\<spacespace> ty list] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50)
translations
--- a/src/HOL/Complex/ex/ReflectedFerrack.thy Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/Complex/ex/ReflectedFerrack.thy Sun Sep 30 21:55:15 2007 +0200
@@ -1908,7 +1908,7 @@
from alluopairs_set1[where xs="?U"] have UpU: "set ?Up \<le> (set ?U \<times> set ?U)" by simp
from uset_l[OF lq] have U_l: "\<forall> (t,n) \<in> set ?U. numbound0 t \<and> n > 0" .
from U_l UpU
- have Up_: "\<forall> ((t,n),(s,m)) \<in> set ?Up. numbound0 t \<and> n> 0 \<and> numbound0 s \<and> m > 0" by auto
+ have "\<forall> ((t,n),(s,m)) \<in> set ?Up. numbound0 t \<and> n> 0 \<and> numbound0 s \<and> m > 0" by auto
hence Snb: "\<forall> (t,n) \<in> set ?S. numbound0 t \<and> n > 0 "
by (auto simp add: mult_pos_pos)
have Y_l: "\<forall> (t,n) \<in> set ?Y. numbound0 t \<and> n > 0"
--- a/src/HOL/MetisExamples/Abstraction.thy Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/MetisExamples/Abstraction.thy Sun Sep 30 21:55:15 2007 +0200
@@ -94,10 +94,10 @@
proof (neg_clausify)
assume 0: "\<And>cl\<Colon>'a\<Colon>type set.
(llabs_subgoal_1\<Colon>'a\<Colon>type set \<Rightarrow> 'a\<Colon>type set) cl =
- Collect (llabs_Set_XCollect_ex_eq_3_ op \<in> (pset cl))"
+ Collect (llabs_Set_XCollect_ex_eq_3 op \<in> (pset cl))"
assume 1: "(f\<Colon>'a\<Colon>type) \<notin> pset (cl\<Colon>'a\<Colon>type set)"
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)"
-have 3: "llabs_Predicate_Xsup_Un_eq2_1_ (CLF\<Colon>('a\<Colon>type set \<times> 'a\<Colon>type) set)
+have 3: "llabs_Predicate_Xsup_Un_eq2_1 (CLF\<Colon>('a\<Colon>type set \<times> 'a\<Colon>type) set)
(cl\<Colon>'a\<Colon>type set) (f\<Colon>'a\<Colon>type)"
by (metis acc_def 2)
assume 4: "(CLF\<Colon>('a\<Colon>type set \<times> 'a\<Colon>type) set) =
@@ -120,7 +120,7 @@
assume 0: "\<And>cl\<Colon>'a\<Colon>type set.
(llabs_subgoal_1\<Colon>'a\<Colon>type set \<Rightarrow> ('a\<Colon>type \<Rightarrow> 'a\<Colon>type) set) cl =
Collect
- (llabs_Set_XCollect_ex_eq_3_ op \<in> (Pi (pset cl) (COMBK (pset cl))))"
+ (llabs_Set_XCollect_ex_eq_3 op \<in> (Pi (pset cl) (COMBK (pset cl))))"
assume 1: "(f\<Colon>'a\<Colon>type \<Rightarrow> 'a\<Colon>type) \<notin> Pi (pset (cl\<Colon>'a\<Colon>type set)) (COMBK (pset cl))"
assume 2: "(cl\<Colon>'a\<Colon>type set, f\<Colon>'a\<Colon>type \<Rightarrow> 'a\<Colon>type)
\<in> Sigma (CL\<Colon>'a\<Colon>type set set)
--- a/src/HOL/MicroJava/J/Conform.thy Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/MicroJava/J/Conform.thy Sun Sep 30 21:55:15 2007 +0200
@@ -8,7 +8,7 @@
theory Conform imports State WellType Exceptions begin
-types 'c env_ = "'c prog \<times> (vname \<rightharpoonup> ty)" -- "same as @{text env} of @{text WellType.thy}"
+types 'c env' = "'c prog \<times> (vname \<rightharpoonup> ty)" -- "same as @{text env} of @{text WellType.thy}"
constdefs
@@ -32,7 +32,7 @@
xconf :: "aheap \<Rightarrow> val option \<Rightarrow> bool"
"xconf hp vo == preallocated hp \<and> (\<forall> v. (vo = Some v) \<longrightarrow> (\<exists> xc. v = (Addr (XcptRef xc))))"
- conforms :: "xstate => java_mb env_ => bool" ("_ ::<= _" [51,51] 50)
+ conforms :: "xstate => java_mb env' => bool" ("_ ::<= _" [51,51] 50)
"s::<=E == prg E|-h heap (store s) [ok] \<and>
prg E,heap (store s)|-locals (store s)[::<=]localT E \<and>
xconf (heap (store s)) (abrupt s)"
@@ -54,7 +54,7 @@
hconf :: "'c prog => aheap => bool"
("_ \<turnstile>h _ \<surd>" [51,51] 50)
- conforms :: "state => java_mb env_ => bool"
+ conforms :: "state => java_mb env' => bool"
("_ ::\<preceq> _" [51,51] 50)
--- a/src/HOL/MicroJava/J/Example.thy Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/MicroJava/J/Example.thy Sun Sep 30 21:55:15 2007 +0200
@@ -37,23 +37,23 @@
\end{verbatim}
*}
-datatype cnam_ = Base_ | Ext_
-datatype vnam_ = vee_ | x_ | e_
+datatype cnam' = Base' | Ext'
+datatype vnam' = vee' | x' | e'
consts
- cnam_ :: "cnam_ => cname"
- vnam_ :: "vnam_ => vnam"
+ cnam' :: "cnam' => cname"
+ vnam' :: "vnam' => vnam"
--- "@{text cnam_} and @{text vnam_} are intended to be isomorphic
+-- "@{text cnam'} and @{text vnam'} are intended to be isomorphic
to @{text cnam} and @{text vnam}"
axioms
- inj_cnam_: "(cnam_ x = cnam_ y) = (x = y)"
- inj_vnam_: "(vnam_ x = vnam_ y) = (x = y)"
+ inj_cnam': "(cnam' x = cnam' y) = (x = y)"
+ inj_vnam': "(vnam' x = vnam' y) = (x = y)"
- surj_cnam_: "\<exists>m. n = cnam_ m"
- surj_vnam_: "\<exists>m. n = vnam_ m"
+ surj_cnam': "\<exists>m. n = cnam' m"
+ surj_vnam': "\<exists>m. n = vnam' m"
-declare inj_cnam_ [simp] inj_vnam_ [simp]
+declare inj_cnam' [simp] inj_vnam' [simp]
syntax
Base :: cname
@@ -63,11 +63,11 @@
e :: vname
translations
- "Base" == "cnam_ Base_"
- "Ext" == "cnam_ Ext_"
- "vee" == "VName (vnam_ vee_)"
- "x" == "VName (vnam_ x_)"
- "e" == "VName (vnam_ e_)"
+ "Base" == "cnam' Base'"
+ "Ext" == "cnam' Ext'"
+ "vee" == "VName (vnam' vee')"
+ "x" == "VName (vnam' x')"
+ "e" == "VName (vnam' e')"
axioms
Base_not_Object: "Base \<noteq> Object"
@@ -220,52 +220,52 @@
declare ty_expr_ty_exprs_wt_stmt.intros [intro!]
-lemma acyclic_subcls1_: "acyclicP (subcls1 tprg)"
+lemma acyclic_subcls1': "acyclicP (subcls1 tprg)"
apply (rule acyclicI [to_pred])
apply safe
done
-lemmas wf_subcls1_ = acyclic_subcls1_ [THEN finite_subcls1 [THEN finite_acyclic_wf_converse [to_pred]]]
+lemmas wf_subcls1' = acyclic_subcls1' [THEN finite_subcls1 [THEN finite_acyclic_wf_converse [to_pred]]]
-lemmas fields_rec_ = wf_subcls1_ [THEN [2] fields_rec_lemma]
+lemmas fields_rec' = wf_subcls1' [THEN [2] fields_rec_lemma]
lemma fields_Object [simp]: "fields (tprg, Object) = []"
-apply (subst fields_rec_)
+apply (subst fields_rec')
apply auto
done
declare is_class_def [simp]
lemma fields_Base [simp]: "fields (tprg,Base) = [((vee, Base), PrimT Boolean)]"
-apply (subst fields_rec_)
+apply (subst fields_rec')
apply auto
done
lemma fields_Ext [simp]:
"fields (tprg, Ext) = [((vee, Ext ), PrimT Integer)] @ fields (tprg, Base)"
apply (rule trans)
-apply (rule fields_rec_)
+apply (rule fields_rec')
apply auto
done
-lemmas method_rec_ = wf_subcls1_ [THEN [2] method_rec_lemma]
+lemmas method_rec' = wf_subcls1' [THEN [2] method_rec_lemma]
lemma method_Object [simp]: "method (tprg,Object) = map_of []"
-apply (subst method_rec_)
+apply (subst method_rec')
apply auto
done
lemma method_Base [simp]: "method (tprg, Base) = map_of
[((foo, [Class Base]), Base, (Class Base, foo_Base))]"
apply (rule trans)
-apply (rule method_rec_)
+apply (rule method_rec')
apply auto
done
lemma method_Ext [simp]: "method (tprg, Ext) = (method (tprg, Base) ++ map_of
[((foo, [Class Base]), Ext , (Class Ext, foo_Ext))])"
apply (rule trans)
-apply (rule method_rec_)
+apply (rule method_rec')
apply auto
done
--- a/src/HOL/MicroJava/J/JBasis.thy Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/MicroJava/J/JBasis.thy Sun Sep 30 21:55:15 2007 +0200
@@ -56,14 +56,14 @@
apply auto
done
-lemma Ball_set_table_:
+lemma Ball_set_table':
"(\<forall>(x,y)\<in>set l. P x y) --> (\<forall>x. \<forall>y. map_of l x = Some y --> P x y)"
apply(induct_tac "l")
apply(simp_all (no_asm))
apply safe
apply auto
done
-lemmas Ball_set_table = Ball_set_table_ [THEN mp];
+lemmas Ball_set_table = Ball_set_table' [THEN mp];
lemma table_of_remap_SomeD [rule_format (no_asm)]:
"map_of (map (\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) -->
--- a/src/HOL/MicroJava/J/JListExample.thy Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/MicroJava/J/JListExample.thy Sun Sep 30 21:55:15 2007 +0200
@@ -62,7 +62,7 @@
cname ("string")
vnam ("string")
mname ("string")
- loc_ ("int")
+ loc' ("int")
consts_code
"new_Addr" ("\<module>new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *} {* Loc *}")
--- a/src/HOL/MicroJava/J/State.thy Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/MicroJava/J/State.thy Sun Sep 30 21:55:15 2007 +0200
@@ -9,9 +9,9 @@
theory State imports TypeRel Value begin
types
- fields_ = "(vname \<times> cname \<rightharpoonup> val)" -- "field name, defining class, value"
+ fields' = "(vname \<times> cname \<rightharpoonup> val)" -- "field name, defining class, value"
- obj = "cname \<times> fields_" -- "class instance with class name and fields"
+ obj = "cname \<times> fields'" -- "class instance with class name and fields"
constdefs
obj_ty :: "obj => ty"
--- a/src/HOL/MicroJava/J/Value.thy Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/MicroJava/J/Value.thy Sun Sep 30 21:55:15 2007 +0200
@@ -8,11 +8,11 @@
theory Value imports Type begin
-typedecl loc_ -- "locations, i.e. abstract references on objects"
+typedecl loc' -- "locations, i.e. abstract references on objects"
datatype loc
= XcptRef xcpt -- "special locations for pre-allocated system exceptions"
- | Loc loc_ -- "usual locations (references on objects)"
+ | Loc loc' -- "usual locations (references on objects)"
datatype val
= Unit -- "dummy result value of void methods"
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy Sun Sep 30 21:55:15 2007 +0200
@@ -91,7 +91,7 @@
cnam ("string")
vnam ("string")
mname ("string")
- loc_ ("int")
+ loc' ("int")
consts_code
"new_Addr" ("\<module>new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}/ {* Loc *}")
--- a/src/ZF/AC/WO6_WO1.thy Sun Sep 30 16:53:08 2007 +0200
+++ b/src/ZF/AC/WO6_WO1.thy Sun Sep 30 21:55:15 2007 +0200
@@ -75,13 +75,13 @@
lemma lam_sets: "f \<in> A->B ==> (\<lambda>x \<in> A. {f`x}): A -> {{b}. b \<in> B}"
by (fast intro!: lam_type apply_type)
-lemma surj_imp_eq_: "f \<in> surj(A,B) ==> (\<Union>a \<in> A. {f`a}) = B"
+lemma surj_imp_eq': "f \<in> surj(A,B) ==> (\<Union>a \<in> A. {f`a}) = B"
apply (unfold surj_def)
apply (fast elim!: apply_type)
done
lemma surj_imp_eq: "[| f \<in> surj(A,B); Ord(A) |] ==> (\<Union>a<A. {f`a}) = B"
-by (fast dest!: surj_imp_eq_ intro!: ltI elim!: ltE)
+by (fast dest!: surj_imp_eq' intro!: ltI elim!: ltE)
lemma WO1_WO4: "WO1 ==> WO4(1)"
apply (unfold WO1_def WO4_def)