--- a/src/HOL/Bali/AxSem.thy Wed Dec 30 19:41:48 2015 +0100
+++ b/src/HOL/Bali/AxSem.thy Wed Dec 30 19:57:37 2015 +0100
@@ -380,34 +380,34 @@
datatype 'a triple = triple "('a assn)" "term" "('a assn)" (** should be
something like triple = \<forall>'a. triple ('a assn) term ('a assn) **)
- ("{(1_)}/ _>/ {(1_)}" [3,65,3]75)
+ ("{(1_)}/ _\<succ>/ {(1_)}" [3,65,3] 75)
type_synonym 'a triples = "'a triple set"
abbreviation
var_triple :: "['a assn, var ,'a assn] \<Rightarrow> 'a triple"
- ("{(1_)}/ _=>/ {(1_)}" [3,80,3] 75)
- where "{P} e=> {Q} == {P} In2 e> {Q}"
+ ("{(1_)}/ _=\<succ>/ {(1_)}" [3,80,3] 75)
+ where "{P} e=\<succ> {Q} == {P} In2 e\<succ> {Q}"
abbreviation
expr_triple :: "['a assn, expr ,'a assn] \<Rightarrow> 'a triple"
- ("{(1_)}/ _->/ {(1_)}" [3,80,3] 75)
- where "{P} e-> {Q} == {P} In1l e> {Q}"
+ ("{(1_)}/ _-\<succ>/ {(1_)}" [3,80,3] 75)
+ where "{P} e-\<succ> {Q} == {P} In1l e\<succ> {Q}"
abbreviation
exprs_triple :: "['a assn, expr list ,'a assn] \<Rightarrow> 'a triple"
- ("{(1_)}/ _#>/ {(1_)}" [3,65,3] 75)
- where "{P} e#> {Q} == {P} In3 e> {Q}"
+ ("{(1_)}/ _\<doteq>\<succ>/ {(1_)}" [3,65,3] 75)
+ where "{P} e\<doteq>\<succ> {Q} == {P} In3 e\<succ> {Q}"
abbreviation
stmt_triple :: "['a assn, stmt, 'a assn] \<Rightarrow> 'a triple"
("{(1_)}/ ._./ {(1_)}" [3,65,3] 75)
- where "{P} .c. {Q} == {P} In1r c> {Q}"
+ where "{P} .c. {Q} == {P} In1r c\<succ> {Q}"
-notation (xsymbols)
- triple ("{(1_)}/ _\<succ>/ {(1_)}" [3,65,3] 75) and
- var_triple ("{(1_)}/ _=\<succ>/ {(1_)}" [3,80,3] 75) and
- expr_triple ("{(1_)}/ _-\<succ>/ {(1_)}" [3,80,3] 75) and
- exprs_triple ("{(1_)}/ _\<doteq>\<succ>/ {(1_)}" [3,65,3] 75)
+notation (ASCII)
+ triple ("{(1_)}/ _>/ {(1_)}" [3,65,3]75) and
+ var_triple ("{(1_)}/ _=>/ {(1_)}" [3,80,3] 75) and
+ expr_triple ("{(1_)}/ _->/ {(1_)}" [3,80,3] 75) and
+ exprs_triple ("{(1_)}/ _#>/ {(1_)}" [3,65,3] 75)
lemma inj_triple: "inj (\<lambda>(P,t,Q). {P} t\<succ> {Q})"
apply (rule inj_onI)
@@ -431,11 +431,11 @@
(\<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" ("_|\<Turnstile>_:_" [61,0, 58] 57)
+ where "G|\<Turnstile>n:ts == Ball ts (triple_valid G n)"
-notation (xsymbols)
- triples_valid ("_|\<Turnstile>_:_" [61,0, 58] 57)
+notation (ASCII)
+ triples_valid ( "_||=_:_" [61,0, 58] 57)
definition
@@ -443,11 +443,11 @@
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" ("_,_\<Turnstile>_" [61,58,58] 57)
+ where "G,A \<Turnstile>t == G,A|\<Turnstile>{t}"
-notation (xsymbols)
- ax_valid ("_,_\<Turnstile>_" [61,58,58] 57)
+notation (ASCII)
+ ax_valid ( "_,_|=_" [61,58,58] 57)
lemma triple_valid_def2: "G\<Turnstile>n:{P} t\<succ> {Q} =
--- a/src/HOL/Bali/Decl.thy Wed Dec 30 19:41:48 2015 +0100
+++ b/src/HOL/Bali/Decl.thy Wed Dec 30 19:57:37 2015 +0100
@@ -456,21 +456,21 @@
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)
- where "G|-C <:C1 D == (C,D) \<in> subcls1 G"
+ subcls1_syntax :: "prog => [qtname, qtname] => bool" ("_\<turnstile>_\<prec>\<^sub>C1_" [71,71,71] 70)
+ where "G\<turnstile>C \<prec>\<^sub>C1 D == (C,D) \<in> subcls1 G"
abbreviation
- subclseq_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<=:C _"[71,71,71] 70)
- where "G|-C <=:C D == (C,D) \<in>(subcls1 G)^*" (* cf. 8.1.3 *)
+ subclseq_syntax :: "prog => [qtname, qtname] => bool" ("_\<turnstile>_\<preceq>\<^sub>C _" [71,71,71] 70)
+ where "G\<turnstile>C \<preceq>\<^sub>C D == (C,D) \<in>(subcls1 G)^*" (* cf. 8.1.3 *)
abbreviation
- subcls_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<:C _"[71,71,71] 70)
- where "G|-C <:C D == (C,D) \<in>(subcls1 G)^+"
+ subcls_syntax :: "prog => [qtname, qtname] => bool" ("_\<turnstile>_\<prec>\<^sub>C _" [71,71,71] 70)
+ where "G\<turnstile>C \<prec>\<^sub>C D == (C,D) \<in>(subcls1 G)^+"
-notation (xsymbols)
- subcls1_syntax ("_\<turnstile>_\<prec>\<^sub>C1_" [71,71,71] 70) and
- subclseq_syntax ("_\<turnstile>_\<preceq>\<^sub>C _" [71,71,71] 70) and
- subcls_syntax ("_\<turnstile>_\<prec>\<^sub>C _" [71,71,71] 70)
+notation (ASCII)
+ subcls1_syntax ("_|-_<:C1_" [71,71,71] 70) and
+ subclseq_syntax ("_|-_<=:C _"[71,71,71] 70) and
+ subcls_syntax ("_|-_<:C _"[71,71,71] 70)
lemma subint1I: "\<lbrakk>iface G I = Some i; J \<in> set (isuperIfs i)\<rbrakk>
\<Longrightarrow> (I,J) \<in> subint1 G"
--- a/src/HOL/Bali/Eval.thy Wed Dec 30 19:41:48 2015 +0100
+++ b/src/HOL/Bali/Eval.thy Wed Dec 30 19:57:37 2015 +0100
@@ -124,7 +124,7 @@
assignment.
*}
-abbreviation (xsymbols)
+abbreviation
dummy_res :: "vals" ("\<diamondsuit>")
where "\<diamondsuit> == In1 Unit"
--- a/src/HOL/Bali/TypeRel.thy Wed Dec 30 19:41:48 2015 +0100
+++ b/src/HOL/Bali/TypeRel.thy Wed Dec 30 19:57:37 2015 +0100
@@ -38,21 +38,21 @@
abbreviation
- subint1_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<:I1_" [71,71,71] 70)
- where "G|-I <:I1 J == (I,J) \<in> subint1 G"
+ subint1_syntax :: "prog => [qtname, qtname] => bool" ("_\<turnstile>_\<prec>I1_" [71,71,71] 70)
+ where "G\<turnstile>I \<prec>I1 J == (I,J) \<in> subint1 G"
abbreviation
- subint_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<=:I _"[71,71,71] 70)
- where "G|-I <=:I J == (I,J) \<in>(subint1 G)^*" --{* cf. 9.1.3 *}
+ subint_syntax :: "prog => [qtname, qtname] => bool" ("_\<turnstile>_\<preceq>I _" [71,71,71] 70)
+ where "G\<turnstile>I \<preceq>I J == (I,J) \<in>(subint1 G)^*" --{* cf. 9.1.3 *}
abbreviation
- implmt1_syntax :: "prog => [qtname, qtname] => bool" ("_|-_~>1_" [71,71,71] 70)
- where "G|-C ~>1 I == (C,I) \<in> implmt1 G"
+ implmt1_syntax :: "prog => [qtname, qtname] => bool" ("_\<turnstile>_\<leadsto>1_" [71,71,71] 70)
+ where "G\<turnstile>C \<leadsto>1 I == (C,I) \<in> implmt1 G"
-notation (xsymbols)
- subint1_syntax ("_\<turnstile>_\<prec>I1_" [71,71,71] 70) and
- subint_syntax ("_\<turnstile>_\<preceq>I _" [71,71,71] 70) and
- implmt1_syntax ("_\<turnstile>_\<leadsto>1_" [71,71,71] 70)
+notation (ASCII)
+ subint1_syntax ("_|-_<:I1_" [71,71,71] 70) and
+ subint_syntax ("_|-_<=:I _"[71,71,71] 70) and
+ implmt1_syntax ("_|-_~>1_" [71,71,71] 70)
subsubsection "subclass and subinterface relations"
--- a/src/HOL/Bali/WellType.thy Wed Dec 30 19:41:48 2015 +0100
+++ b/src/HOL/Bali/WellType.thy Wed Dec 30 19:57:37 2015 +0100
@@ -429,31 +429,31 @@
(* for purely static typing *)
abbreviation
- wt_syntax :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
- where "E|-t::T == E,empty_dt\<Turnstile>t\<Colon> T"
+ wt_syntax :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>_" [51,51,51] 50)
+ where "E\<turnstile>t\<Colon>T == E,empty_dt\<Turnstile>t\<Colon> T"
abbreviation
- wt_stmt_syntax :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_|-_:<>" [51,51 ] 50)
- where "E|-s:<> == E|-In1r s :: Inl (PrimT Void)"
+ wt_stmt_syntax :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<surd>" [51,51 ] 50)
+ where "E\<turnstile>s\<Colon>\<surd> == E\<turnstile>In1r s \<Colon> Inl (PrimT Void)"
abbreviation
- ty_expr_syntax :: "env \<Rightarrow> [expr, ty] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50)
- where "E|-e:-T == E|-In1l e :: Inl T"
+ ty_expr_syntax :: "env \<Rightarrow> [expr, ty] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>-_" [51,51,51] 50)
+ where "E\<turnstile>e\<Colon>-T == E\<turnstile>In1l e \<Colon> Inl T"
abbreviation
- ty_var_syntax :: "env \<Rightarrow> [var, ty] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50)
- where "E|-e:=T == E|-In2 e :: Inl T"
+ ty_var_syntax :: "env \<Rightarrow> [var, ty] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>=_" [51,51,51] 50)
+ where "E\<turnstile>e\<Colon>=T == E\<turnstile>In2 e \<Colon> Inl T"
abbreviation
- ty_exprs_syntax :: "env \<Rightarrow> [expr list, ty list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50)
- where "E|-e:#T == E|-In3 e :: Inr T"
+ ty_exprs_syntax :: "env \<Rightarrow> [expr list, ty list] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50)
+ where "E\<turnstile>e\<Colon>\<doteq>T == E\<turnstile>In3 e \<Colon> Inr T"
-notation (xsymbols)
- wt_syntax ("_\<turnstile>_\<Colon>_" [51,51,51] 50) and
- wt_stmt_syntax ("_\<turnstile>_\<Colon>\<surd>" [51,51 ] 50) and
- ty_expr_syntax ("_\<turnstile>_\<Colon>-_" [51,51,51] 50) and
- ty_var_syntax ("_\<turnstile>_\<Colon>=_" [51,51,51] 50) and
- ty_exprs_syntax ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50)
+notation (ASCII)
+ wt_syntax ("_|-_::_" [51,51,51] 50) and
+ wt_stmt_syntax ("_|-_:<>" [51,51 ] 50) and
+ ty_expr_syntax ("_|-_:-_" [51,51,51] 50) and
+ ty_var_syntax ("_|-_:=_" [51,51,51] 50) and
+ ty_exprs_syntax ("_|-_:#_" [51,51,51] 50)
declare not_None_eq [simp del]
declare split_if [split del] split_if_asm [split del]