# HG changeset patch # User wenzelm # Date 1451501857 -3600 # Node ID ba8c284d47251a49482d7b5539513e1fcbf8c5bb # Parent 34b51f436e929db5e8d8567248522938977a1d5c clarified print modes; diff -r 34b51f436e92 -r ba8c284d4725 src/HOL/Bali/AxSem.thy --- 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 = \'a. triple ('a assn) term ('a assn) **) - ("{(1_)}/ _>/ {(1_)}" [3,65,3]75) + ("{(1_)}/ _\/ {(1_)}" [3,65,3] 75) type_synonym 'a triples = "'a triple set" abbreviation var_triple :: "['a assn, var ,'a assn] \ 'a triple" - ("{(1_)}/ _=>/ {(1_)}" [3,80,3] 75) - where "{P} e=> {Q} == {P} In2 e> {Q}" + ("{(1_)}/ _=\/ {(1_)}" [3,80,3] 75) + where "{P} e=\ {Q} == {P} In2 e\ {Q}" abbreviation expr_triple :: "['a assn, expr ,'a assn] \ 'a triple" - ("{(1_)}/ _->/ {(1_)}" [3,80,3] 75) - where "{P} e-> {Q} == {P} In1l e> {Q}" + ("{(1_)}/ _-\/ {(1_)}" [3,80,3] 75) + where "{P} e-\ {Q} == {P} In1l e\ {Q}" abbreviation exprs_triple :: "['a assn, expr list ,'a assn] \ 'a triple" - ("{(1_)}/ _#>/ {(1_)}" [3,65,3] 75) - where "{P} e#> {Q} == {P} In3 e> {Q}" + ("{(1_)}/ _\\/ {(1_)}" [3,65,3] 75) + where "{P} e\\ {Q} == {P} In3 e\ {Q}" abbreviation stmt_triple :: "['a assn, stmt, 'a assn] \ 'a triple" ("{(1_)}/ ._./ {(1_)}" [3,65,3] 75) - where "{P} .c. {Q} == {P} In1r c> {Q}" + where "{P} .c. {Q} == {P} In1r c\ {Q}" -notation (xsymbols) - 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) +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 (\(P,t,Q). {P} t\ {Q})" apply (rule inj_onI) @@ -431,11 +431,11 @@ (\Y' s'. G\s \t\\n\ (Y',s') \ Q Y' s' Z))" abbreviation - triples_valid:: "prog \ nat \ 'a triples \ bool" ( "_||=_:_" [61,0, 58] 57) - where "G||=n:ts == Ball ts (triple_valid G n)" + triples_valid:: "prog \ nat \ 'a triples \ bool" ("_|\_:_" [61,0, 58] 57) + where "G|\n:ts == Ball ts (triple_valid G n)" -notation (xsymbols) - triples_valid ("_|\_:_" [61,0, 58] 57) +notation (ASCII) + triples_valid ( "_||=_:_" [61,0, 58] 57) definition @@ -443,11 +443,11 @@ where "(G,A|\ts) = (\n. G|\n:A \ G|\n:ts)" abbreviation - ax_valid :: "prog \ 'b triples \ 'a triple \ bool" ( "_,_|=_" [61,58,58] 57) - where "G,A |=t == G,A|\{t}" + ax_valid :: "prog \ 'b triples \ 'a triple \ bool" ("_,_\_" [61,58,58] 57) + where "G,A \t == G,A|\{t}" -notation (xsymbols) - ax_valid ("_,_\_" [61,58,58] 57) +notation (ASCII) + ax_valid ( "_,_|=_" [61,58,58] 57) lemma triple_valid_def2: "G\n:{P} t\ {Q} = diff -r 34b51f436e92 -r ba8c284d4725 src/HOL/Bali/Decl.thy --- 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\Object \ (\c\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) \ subcls1 G" + subcls1_syntax :: "prog => [qtname, qtname] => bool" ("_\_\\<^sub>C1_" [71,71,71] 70) + where "G\C \\<^sub>C1 D == (C,D) \ subcls1 G" abbreviation - subclseq_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<=:C _"[71,71,71] 70) - where "G|-C <=:C D == (C,D) \(subcls1 G)^*" (* cf. 8.1.3 *) + subclseq_syntax :: "prog => [qtname, qtname] => bool" ("_\_\\<^sub>C _" [71,71,71] 70) + where "G\C \\<^sub>C D == (C,D) \(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) \(subcls1 G)^+" + subcls_syntax :: "prog => [qtname, qtname] => bool" ("_\_\\<^sub>C _" [71,71,71] 70) + where "G\C \\<^sub>C D == (C,D) \(subcls1 G)^+" -notation (xsymbols) - subcls1_syntax ("_\_\\<^sub>C1_" [71,71,71] 70) and - subclseq_syntax ("_\_\\<^sub>C _" [71,71,71] 70) and - subcls_syntax ("_\_\\<^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: "\iface G I = Some i; J \ set (isuperIfs i)\ \ (I,J) \ subint1 G" diff -r 34b51f436e92 -r ba8c284d4725 src/HOL/Bali/Eval.thy --- 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" ("\") where "\ == In1 Unit" diff -r 34b51f436e92 -r ba8c284d4725 src/HOL/Bali/TypeRel.thy --- 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) \ subint1 G" + subint1_syntax :: "prog => [qtname, qtname] => bool" ("_\_\I1_" [71,71,71] 70) + where "G\I \I1 J == (I,J) \ subint1 G" abbreviation - subint_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<=:I _"[71,71,71] 70) - where "G|-I <=:I J == (I,J) \(subint1 G)^*" --{* cf. 9.1.3 *} + subint_syntax :: "prog => [qtname, qtname] => bool" ("_\_\I _" [71,71,71] 70) + where "G\I \I J == (I,J) \(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) \ implmt1 G" + implmt1_syntax :: "prog => [qtname, qtname] => bool" ("_\_\1_" [71,71,71] 70) + where "G\C \1 I == (C,I) \ implmt1 G" -notation (xsymbols) - subint1_syntax ("_\_\I1_" [71,71,71] 70) and - subint_syntax ("_\_\I _" [71,71,71] 70) and - implmt1_syntax ("_\_\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" diff -r 34b51f436e92 -r ba8c284d4725 src/HOL/Bali/WellType.thy --- 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 \ [term,tys] \ bool" ("_|-_::_" [51,51,51] 50) - where "E|-t::T == E,empty_dt\t\ T" + wt_syntax :: "env \ [term,tys] \ bool" ("_\_\_" [51,51,51] 50) + where "E\t\T == E,empty_dt\t\ T" abbreviation - wt_stmt_syntax :: "env \ stmt \ bool" ("_|-_:<>" [51,51 ] 50) - where "E|-s:<> == E|-In1r s :: Inl (PrimT Void)" + wt_stmt_syntax :: "env \ stmt \ bool" ("_\_\\" [51,51 ] 50) + where "E\s\\ == E\In1r s \ Inl (PrimT Void)" abbreviation - ty_expr_syntax :: "env \ [expr, ty] \ bool" ("_|-_:-_" [51,51,51] 50) - where "E|-e:-T == E|-In1l e :: Inl T" + ty_expr_syntax :: "env \ [expr, ty] \ bool" ("_\_\-_" [51,51,51] 50) + where "E\e\-T == E\In1l e \ Inl T" abbreviation - ty_var_syntax :: "env \ [var, ty] \ bool" ("_|-_:=_" [51,51,51] 50) - where "E|-e:=T == E|-In2 e :: Inl T" + ty_var_syntax :: "env \ [var, ty] \ bool" ("_\_\=_" [51,51,51] 50) + where "E\e\=T == E\In2 e \ Inl T" abbreviation - ty_exprs_syntax :: "env \ [expr list, ty list] \ bool" ("_|-_:#_" [51,51,51] 50) - where "E|-e:#T == E|-In3 e :: Inr T" + ty_exprs_syntax :: "env \ [expr list, ty list] \ bool" ("_\_\\_" [51,51,51] 50) + where "E\e\\T == E\In3 e \ Inr T" -notation (xsymbols) - 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) +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]