modernized syntax declarations, and make them actually work with authentic syntax;
authorwenzelm
Wed Feb 24 22:09:50 2010 +0100 (2010-02-24)
changeset 35355613e133966ea
parent 35354 2e8dc3c64430
child 35357 413f9ba7e308
modernized syntax declarations, and make them actually work with authentic syntax;
src/HOL/Algebra/Congruence.thy
src/HOL/Bali/Basis.thy
src/HOL/Bali/Table.thy
src/HOL/Isar_Examples/Hoare.thy
src/HOL/MicroJava/BV/Correct.thy
src/HOL/MicroJava/BV/JVMType.thy
src/HOL/MicroJava/Comp/TranslCompTp.thy
src/HOL/MicroJava/DFA/Semilat.thy
src/HOL/MicroJava/J/Conform.thy
src/HOL/MicroJava/JVM/JVMDefensive.thy
src/HOL/MicroJava/JVM/JVMExec.thy
src/HOL/NanoJava/Equivalence.thy
src/HOL/NanoJava/State.thy
src/HOL/UNITY/SubstAx.thy
src/HOL/UNITY/WFair.thy
src/HOLCF/IOA/meta_theory/Pred.thy
src/Sequents/LK0.thy
     1.1 --- a/src/HOL/Algebra/Congruence.thy	Wed Feb 24 22:04:10 2010 +0100
     1.2 +++ b/src/HOL/Algebra/Congruence.thy	Wed Feb 24 22:09:50 2010 +0100
     1.3 @@ -35,15 +35,17 @@
     1.4    eq_is_closed :: "_ \<Rightarrow> 'a set \<Rightarrow> bool" ("is'_closed\<index> _")
     1.5    "is_closed A == (A \<subseteq> carrier S \<and> closure_of A = A)"
     1.6  
     1.7 -syntax
     1.8 +abbreviation
     1.9    not_eq :: "_ \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl ".\<noteq>\<index>" 50)
    1.10 -  not_elem :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixl ".\<notin>\<index>" 50)
    1.11 -  set_not_eq :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "{.\<noteq>}\<index>" 50)
    1.12 +  where "x .\<noteq>\<^bsub>S\<^esub> y == ~(x .=\<^bsub>S\<^esub> y)"
    1.13  
    1.14 -translations
    1.15 -  "x .\<noteq>\<index> y" == "~(x .=\<index> y)"
    1.16 -  "x .\<notin>\<index> A" == "~(x .\<in>\<index> A)"
    1.17 -  "A {.\<noteq>}\<index> B" == "~(A {.=}\<index> B)"
    1.18 +abbreviation
    1.19 +  not_elem :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixl ".\<notin>\<index>" 50)
    1.20 +  where "x .\<notin>\<^bsub>S\<^esub> A == ~(x .\<in>\<^bsub>S\<^esub> A)"
    1.21 +
    1.22 +abbreviation
    1.23 +  set_not_eq :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "{.\<noteq>}\<index>" 50)
    1.24 +  where "A {.\<noteq>}\<^bsub>S\<^esub> B == ~(A {.=}\<^bsub>S\<^esub> B)"
    1.25  
    1.26  locale equivalence =
    1.27    fixes S (structure)
     2.1 --- a/src/HOL/Bali/Basis.thy	Wed Feb 24 22:04:10 2010 +0100
     2.2 +++ b/src/HOL/Bali/Basis.thy	Wed Feb 24 22:09:50 2010 +0100
     2.3 @@ -222,12 +222,12 @@
     2.4  section "quantifiers for option type"
     2.5  
     2.6  syntax
     2.7 -  Oall :: "[pttrn, 'a option, bool] => bool"   ("(3! _:_:/ _)" [0,0,10] 10)
     2.8 -  Oex  :: "[pttrn, 'a option, bool] => bool"   ("(3? _:_:/ _)" [0,0,10] 10)
     2.9 +  "_Oall" :: "[pttrn, 'a option, bool] => bool"   ("(3! _:_:/ _)" [0,0,10] 10)
    2.10 +  "_Oex"  :: "[pttrn, 'a option, bool] => bool"   ("(3? _:_:/ _)" [0,0,10] 10)
    2.11  
    2.12  syntax (symbols)
    2.13 -  Oall :: "[pttrn, 'a option, bool] => bool"   ("(3\<forall>_\<in>_:/ _)"  [0,0,10] 10)
    2.14 -  Oex  :: "[pttrn, 'a option, bool] => bool"   ("(3\<exists>_\<in>_:/ _)"  [0,0,10] 10)
    2.15 +  "_Oall" :: "[pttrn, 'a option, bool] => bool"   ("(3\<forall>_\<in>_:/ _)"  [0,0,10] 10)
    2.16 +  "_Oex"  :: "[pttrn, 'a option, bool] => bool"   ("(3\<exists>_\<in>_:/ _)"  [0,0,10] 10)
    2.17  
    2.18  translations
    2.19    "! x:A: P"    == "! x:CONST Option.set A. P"
     3.1 --- a/src/HOL/Bali/Table.thy	Wed Feb 24 22:04:10 2010 +0100
     3.2 +++ b/src/HOL/Bali/Table.thy	Wed Feb 24 22:09:50 2010 +0100
     3.3 @@ -37,11 +37,9 @@
     3.4  
     3.5  section "map of / table of"
     3.6  
     3.7 -syntax
     3.8 -  table_of      :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table"   --{* concrete table *}
     3.9 -  
    3.10  abbreviation
    3.11 -  "table_of \<equiv> map_of"
    3.12 +  table_of :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table"   --{* concrete table *}
    3.13 +  where "table_of \<equiv> map_of"
    3.14  
    3.15  translations
    3.16    (type)"'a \<rightharpoonup> 'b"       <= (type)"'a \<Rightarrow> 'b Datatype.option"
     4.1 --- a/src/HOL/Isar_Examples/Hoare.thy	Wed Feb 24 22:04:10 2010 +0100
     4.2 +++ b/src/HOL/Isar_Examples/Hoare.thy	Wed Feb 24 22:09:50 2010 +0100
     4.3 @@ -60,9 +60,8 @@
     4.4      ("(3|- _/ (2_)/ _)" [100, 55, 100] 50)
     4.5    "|- P c Q == ALL s s'. Sem c s s' --> s : P --> s' : Q"
     4.6  
     4.7 -syntax (xsymbols)
     4.8 -  Valid :: "'a bexp => 'a com => 'a bexp => bool"
     4.9 -    ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)
    4.10 +notation (xsymbols)
    4.11 +  Valid  ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)
    4.12  
    4.13  lemma ValidI [intro?]:
    4.14      "(!!s s'. Sem c s s' ==> s : P ==> s' : Q) ==> |- P c Q"
     5.1 --- a/src/HOL/MicroJava/BV/Correct.thy	Wed Feb 24 22:04:10 2010 +0100
     5.2 +++ b/src/HOL/MicroJava/BV/Correct.thy	Wed Feb 24 22:09:50 2010 +0100
     5.3 @@ -66,9 +66,8 @@
     5.4     | Some x \<Rightarrow> frs = []" 
     5.5  
     5.6  
     5.7 -syntax (xsymbols)
     5.8 - correct_state :: "[jvm_prog,prog_type,jvm_state] \<Rightarrow> bool"
     5.9 -                  ("_,_ \<turnstile>JVM _ \<surd>"  [51,51] 50)
    5.10 +notation (xsymbols)
    5.11 + correct_state  ("_,_ \<turnstile>JVM _ \<surd>"  [51,51] 50)
    5.12  
    5.13  
    5.14  lemma sup_ty_opt_OK:
     6.1 --- a/src/HOL/MicroJava/BV/JVMType.thy	Wed Feb 24 22:04:10 2010 +0100
     6.2 +++ b/src/HOL/MicroJava/BV/JVMType.thy	Wed Feb 24 22:09:50 2010 +0100
     6.3 @@ -59,15 +59,11 @@
     6.4    "sup_state_opt G == Opt.le (sup_state G)"
     6.5  
     6.6  
     6.7 -syntax (xsymbols)
     6.8 -  sup_ty_opt    :: "['code prog,ty err,ty err] \<Rightarrow> bool" 
     6.9 -                   ("_ \<turnstile> _ <=o _" [71,71] 70)
    6.10 -  sup_loc       :: "['code prog,locvars_type,locvars_type] \<Rightarrow> bool" 
    6.11 -                   ("_ \<turnstile> _ <=l _" [71,71] 70)
    6.12 -  sup_state     :: "['code prog,state_type,state_type] \<Rightarrow> bool" 
    6.13 -                   ("_ \<turnstile> _ <=s _" [71,71] 70)
    6.14 -  sup_state_opt :: "['code prog,state_type option,state_type option] \<Rightarrow> bool"
    6.15 -                   ("_ \<turnstile> _ <=' _" [71,71] 70)
    6.16 +notation (xsymbols)
    6.17 +  sup_ty_opt  ("_ \<turnstile> _ <=o _" [71,71] 70) and
    6.18 +  sup_loc  ("_ \<turnstile> _ <=l _" [71,71] 70) and
    6.19 +  sup_state  ("_ \<turnstile> _ <=s _" [71,71] 70) and
    6.20 +  sup_state_opt  ("_ \<turnstile> _ <=' _" [71,71] 70)
    6.21                     
    6.22  
    6.23  lemma JVM_states_unfold: 
     7.1 --- a/src/HOL/MicroJava/Comp/TranslCompTp.thy	Wed Feb 24 22:04:10 2010 +0100
     7.2 +++ b/src/HOL/MicroJava/Comp/TranslCompTp.thy	Wed Feb 24 22:09:50 2010 +0100
     7.3 @@ -19,9 +19,8 @@
     7.4    comb_nil :: "'a \<Rightarrow> 'b list \<times> 'a"
     7.5    "comb_nil a == ([], a)"
     7.6  
     7.7 -syntax (xsymbols)
     7.8 -  "comb" :: "['a \<Rightarrow> 'b list \<times> 'c, 'c \<Rightarrow> 'b list \<times> 'd, 'a] \<Rightarrow> 'b list \<times> 'd"    
     7.9 -            (infixr "\<box>" 55)
    7.10 +notation (xsymbols)
    7.11 +  comb  (infixr "\<box>" 55)
    7.12  
    7.13  lemma comb_nil_left [simp]: "comb_nil \<box> f = f"
    7.14  by (simp add: comb_def comb_nil_def split_beta)
     8.1 --- a/src/HOL/MicroJava/DFA/Semilat.thy	Wed Feb 24 22:04:10 2010 +0100
     8.2 +++ b/src/HOL/MicroJava/DFA/Semilat.thy	Wed Feb 24 22:09:50 2010 +0100
     8.3 @@ -32,16 +32,19 @@
     8.4    "lesssub"  ("(_ /\<sqsubset>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and
     8.5    "plussub"  ("(_ /\<squnion>\<^bsub>_\<^esub> _)" [65, 0, 66] 65)
     8.6  (*<*)
     8.7 -syntax
     8.8 - (* allow \<sub> instead of \<bsub>..\<esub> *)  
     8.9 -  "_lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubseteq>\<^sub>_ _)" [50, 1000, 51] 50)
    8.10 -  "_lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubset>\<^sub>_ _)" [50, 1000, 51] 50)
    8.11 -  "_plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^sub>_ _)" [65, 1000, 66] 65)
    8.12 +(* allow \<sub> instead of \<bsub>..\<esub> *)
    8.13 +
    8.14 +abbreviation (input)
    8.15 +  lesub1 :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubseteq>\<^sub>_ _)" [50, 1000, 51] 50)
    8.16 +  where "x \<sqsubseteq>\<^sub>r y == x \<sqsubseteq>\<^bsub>r\<^esub> y"
    8.17  
    8.18 -translations
    8.19 -  "x \<sqsubseteq>\<^sub>r y" => "x \<sqsubseteq>\<^bsub>r\<^esub> y"
    8.20 -  "x \<sqsubset>\<^sub>r y" => "x \<sqsubset>\<^bsub>r\<^esub> y" 
    8.21 -  "x \<squnion>\<^sub>f y" => "x \<squnion>\<^bsub>f\<^esub> y" 
    8.22 +abbreviation (input)
    8.23 +  lesssub1 :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubset>\<^sub>_ _)" [50, 1000, 51] 50)
    8.24 +  where "x \<sqsubset>\<^sub>r y == x \<sqsubset>\<^bsub>r\<^esub> y"
    8.25 +
    8.26 +abbreviation (input)
    8.27 +  plussub1 :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^sub>_ _)" [65, 1000, 66] 65)
    8.28 +  where "x \<squnion>\<^sub>f y == x \<squnion>\<^bsub>f\<^esub> y"
    8.29  (*>*)
    8.30  
    8.31  defs
     9.1 --- a/src/HOL/MicroJava/J/Conform.thy	Wed Feb 24 22:04:10 2010 +0100
     9.2 +++ b/src/HOL/MicroJava/J/Conform.thy	Wed Feb 24 22:09:50 2010 +0100
     9.3 @@ -38,24 +38,13 @@
     9.4              xconf (heap (store s)) (abrupt s)"
     9.5  
     9.6  
     9.7 -syntax (xsymbols)
     9.8 -  hext     :: "aheap => aheap => bool"
     9.9 -              ("_ \<le>| _" [51,51] 50)
    9.10 -
    9.11 -  conf     :: "'c prog => aheap => val => ty => bool"
    9.12 -              ("_,_ \<turnstile> _ ::\<preceq> _" [51,51,51,51] 50)
    9.13 -
    9.14 -  lconf    :: "'c prog => aheap => ('a \<rightharpoonup> val) => ('a \<rightharpoonup> ty) => bool"
    9.15 -              ("_,_ \<turnstile> _ [::\<preceq>] _" [51,51,51,51] 50)
    9.16 -
    9.17 -  oconf    :: "'c prog => aheap => obj => bool"
    9.18 -              ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50)
    9.19 -
    9.20 -  hconf    :: "'c prog => aheap => bool"
    9.21 -              ("_ \<turnstile>h _ \<surd>" [51,51] 50)
    9.22 -
    9.23 -  conforms :: "state => java_mb env' => bool"
    9.24 -              ("_ ::\<preceq> _" [51,51] 50)
    9.25 +notation (xsymbols)
    9.26 +  hext  ("_ \<le>| _" [51,51] 50) and
    9.27 +  conf  ("_,_ \<turnstile> _ ::\<preceq> _" [51,51,51,51] 50) and
    9.28 +  lconf  ("_,_ \<turnstile> _ [::\<preceq>] _" [51,51,51,51] 50) and
    9.29 +  oconf  ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50) and
    9.30 +  hconf  ("_ \<turnstile>h _ \<surd>" [51,51] 50) and
    9.31 +  conforms  ("_ ::\<preceq> _" [51,51] 50)
    9.32  
    9.33  
    9.34  section "hext"
    10.1 --- a/src/HOL/MicroJava/JVM/JVMDefensive.thy	Wed Feb 24 22:04:10 2010 +0100
    10.2 +++ b/src/HOL/MicroJava/JVM/JVMDefensive.thy	Wed Feb 24 22:09:50 2010 +0100
    10.3 @@ -123,19 +123,15 @@
    10.4      | Normal s' \<Rightarrow> if check G s' then Normal (exec (G, s')) else TypeError"
    10.5  
    10.6  
    10.7 -consts
    10.8 -  "exec_all_d" :: "jvm_prog \<Rightarrow> jvm_state type_error \<Rightarrow> jvm_state type_error \<Rightarrow> bool" 
    10.9 +constdefs
   10.10 +  exec_all_d :: "jvm_prog \<Rightarrow> jvm_state type_error \<Rightarrow> jvm_state type_error \<Rightarrow> bool" 
   10.11                     ("_ |- _ -jvmd-> _" [61,61,61]60)
   10.12 +  "G |- s -jvmd-> t \<equiv>
   10.13 +         (s,t) \<in> ({(s,t). exec_d G s = TypeError \<and> t = TypeError} \<union>
   10.14 +                  {(s,t). \<exists>t'. exec_d G s = Normal (Some t') \<and> t = Normal t'})\<^sup>*"
   10.15  
   10.16 -syntax (xsymbols)
   10.17 -  "exec_all_d" :: "jvm_prog \<Rightarrow> jvm_state type_error \<Rightarrow> jvm_state type_error \<Rightarrow> bool" 
   10.18 -                   ("_ \<turnstile> _ -jvmd\<rightarrow> _" [61,61,61]60)  
   10.19 - 
   10.20 -defs
   10.21 -  exec_all_d_def:
   10.22 -  "G \<turnstile> s -jvmd\<rightarrow> t \<equiv>
   10.23 -         (s,t) \<in> ({(s,t). exec_d G s = TypeError \<and> t = TypeError} \<union> 
   10.24 -                  {(s,t). \<exists>t'. exec_d G s = Normal (Some t') \<and> t = Normal t'})\<^sup>*"
   10.25 +notation (xsymbols)
   10.26 +  exec_all_d  ("_ \<turnstile> _ -jvmd\<rightarrow> _" [61,61,61]60)
   10.27  
   10.28  
   10.29  declare split_paired_All [simp del]
    11.1 --- a/src/HOL/MicroJava/JVM/JVMExec.thy	Wed Feb 24 22:04:10 2010 +0100
    11.2 +++ b/src/HOL/MicroJava/JVM/JVMExec.thy	Wed Feb 24 22:09:50 2010 +0100
    11.3 @@ -32,9 +32,8 @@
    11.4    "G |- s -jvm-> t == (s,t) \<in> {(s,t). exec(G,s) = Some t}^*"
    11.5  
    11.6  
    11.7 -syntax (xsymbols)
    11.8 -  exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"
    11.9 -              ("_ \<turnstile> _ -jvm\<rightarrow> _" [61,61,61]60)
   11.10 +notation (xsymbols)
   11.11 +  exec_all  ("_ \<turnstile> _ -jvm\<rightarrow> _" [61,61,61]60)
   11.12  
   11.13  text {*
   11.14    The start configuration of the JVM: in the start heap, we call a 
    12.1 --- a/src/HOL/NanoJava/Equivalence.thy	Wed Feb 24 22:04:10 2010 +0100
    12.2 +++ b/src/HOL/NanoJava/Equivalence.thy	Wed Feb 24 22:09:50 2010 +0100
    12.3 @@ -33,14 +33,14 @@
    12.4  cenvalid  :: "[triple set,etriple   ] => bool" ("_ ||=e/ _" [61,61] 60)
    12.5   "A ||=e t \<equiv> \<forall>n. ||=n: A --> |=n:e t"
    12.6  
    12.7 -syntax (xsymbols)
    12.8 -   valid  :: "[assn,stmt, assn] => bool" ( "\<Turnstile> {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
    12.9 -  evalid  :: "[assn,expr,vassn] => bool" ("\<Turnstile>\<^sub>e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
   12.10 -  nvalid  :: "[nat, triple          ] => bool" ("\<Turnstile>_: _"  [61,61] 60)
   12.11 - envalid  :: "[nat,etriple          ] => bool" ("\<Turnstile>_:\<^sub>e _" [61,61] 60)
   12.12 -  nvalids :: "[nat,       triple set] => bool" ("|\<Turnstile>_: _"  [61,61] 60)
   12.13 - cnvalids :: "[triple set,triple set] => bool" ("_ |\<Turnstile>/ _" [61,61] 60)
   12.14 -cenvalid  :: "[triple set,etriple   ] => bool" ("_ |\<Turnstile>\<^sub>e/ _"[61,61] 60)
   12.15 +notation (xsymbols)
   12.16 +  valid  ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) and
   12.17 +  evalid  ("\<Turnstile>\<^sub>e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) and
   12.18 +  nvalid  ("\<Turnstile>_: _" [61,61] 60) and
   12.19 +  envalid  ("\<Turnstile>_:\<^sub>e _" [61,61] 60) and
   12.20 +  nvalids  ("|\<Turnstile>_: _" [61,61] 60) and
   12.21 +  cnvalids  ("_ |\<Turnstile>/ _" [61,61] 60) and
   12.22 +  cenvalid  ("_ |\<Turnstile>\<^sub>e/ _"[61,61] 60)
   12.23  
   12.24  
   12.25  lemma nvalid_def2: "\<Turnstile>n: (P,c,Q) \<equiv> \<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t"
   12.26 @@ -164,10 +164,10 @@
   12.27           "MGT  c Z \<equiv> (\<lambda>s. Z = s, c, \<lambda>  t. \<exists>n. Z -c-  n\<rightarrow> t)"
   12.28            MGTe   :: "expr => state => etriple"
   12.29           "MGTe e Z \<equiv> (\<lambda>s. Z = s, e, \<lambda>v t. \<exists>n. Z -e\<succ>v-n\<rightarrow> t)"
   12.30 -syntax (xsymbols)
   12.31 -         MGTe    :: "expr => state => etriple" ("MGT\<^sub>e")
   12.32 -syntax (HTML output)
   12.33 -         MGTe    :: "expr => state => etriple" ("MGT\<^sub>e")
   12.34 +notation (xsymbols)
   12.35 +  MGTe  ("MGT\<^sub>e")
   12.36 +notation (HTML output)
   12.37 +  MGTe  ("MGT\<^sub>e")
   12.38  
   12.39  lemma MGF_implies_complete:
   12.40   "\<forall>Z. {} |\<turnstile> { MGT c Z} \<Longrightarrow> \<Turnstile>  {P} c {Q} \<Longrightarrow> {} \<turnstile>  {P} c {Q}"
    13.1 --- a/src/HOL/NanoJava/State.thy	Wed Feb 24 22:04:10 2010 +0100
    13.2 +++ b/src/HOL/NanoJava/State.thy	Wed Feb 24 22:09:50 2010 +0100
    13.3 @@ -84,9 +84,9 @@
    13.4    lupd       :: "vname => val => state => state" ("lupd'(_|->_')" [10,10] 1000)
    13.5   "lupd x v s   \<equiv> s (| locals := ((locals s)(x\<mapsto>v  ))|)"
    13.6  
    13.7 -syntax (xsymbols)
    13.8 -  hupd       :: "loc => obj => state => state"   ("hupd'(_\<mapsto>_')" [10,10] 1000)
    13.9 -  lupd       :: "vname => val => state => state" ("lupd'(_\<mapsto>_')" [10,10] 1000)
   13.10 +notation (xsymbols)
   13.11 +  hupd  ("hupd'(_\<mapsto>_')" [10,10] 1000) and
   13.12 +  lupd  ("lupd'(_\<mapsto>_')" [10,10] 1000)
   13.13  
   13.14  constdefs
   13.15  
    14.1 --- a/src/HOL/UNITY/SubstAx.thy	Wed Feb 24 22:04:10 2010 +0100
    14.2 +++ b/src/HOL/UNITY/SubstAx.thy	Wed Feb 24 22:09:50 2010 +0100
    14.3 @@ -17,8 +17,8 @@
    14.4     LeadsTo :: "['a set, 'a set] => 'a program set"    (infixl "LeadsTo" 60)
    14.5      "A LeadsTo B == {F. F \<in> (reachable F \<inter> A) leadsTo B}"
    14.6  
    14.7 -syntax (xsymbols)
    14.8 -  "op LeadsTo" :: "['a set, 'a set] => 'a program set" (infixl " \<longmapsto>w " 60)
    14.9 +notation (xsymbols)
   14.10 +  LeadsTo  (infixl " \<longmapsto>w " 60)
   14.11  
   14.12  
   14.13  text{*Resembles the previous definition of LeadsTo*}
    15.1 --- a/src/HOL/UNITY/WFair.thy	Wed Feb 24 22:04:10 2010 +0100
    15.2 +++ b/src/HOL/UNITY/WFair.thy	Wed Feb 24 22:09:50 2010 +0100
    15.3 @@ -69,8 +69,8 @@
    15.4       --{*predicate transformer: the largest set that leads to @{term B}*}
    15.5      "wlt F B == Union {A. F \<in> A leadsTo B}"
    15.6  
    15.7 -syntax (xsymbols)
    15.8 -  "op leadsTo" :: "['a set, 'a set] => 'a program set" (infixl "\<longmapsto>" 60)
    15.9 +notation (xsymbols)
   15.10 +  leadsTo  (infixl "\<longmapsto>" 60)
   15.11  
   15.12  
   15.13  subsection{*transient*}
    16.1 --- a/src/HOLCF/IOA/meta_theory/Pred.thy	Wed Feb 24 22:04:10 2010 +0100
    16.2 +++ b/src/HOLCF/IOA/meta_theory/Pred.thy	Wed Feb 24 22:09:50 2010 +0100
    16.3 @@ -24,25 +24,25 @@
    16.4  IMPLIES      ::"'a predicate => 'a predicate => 'a predicate"    (infixr ".-->" 25)
    16.5  
    16.6  
    16.7 -syntax ("" output)
    16.8 -  "NOT"     ::"'a predicate => 'a predicate" ("~ _" [40] 40)
    16.9 -  "AND"     ::"'a predicate => 'a predicate => 'a predicate"    (infixr "&" 35)
   16.10 -  "OR"      ::"'a predicate => 'a predicate => 'a predicate"    (infixr "|" 30)
   16.11 -  "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate"    (infixr "-->" 25)
   16.12 +notation (output)
   16.13 +  NOT  ("~ _" [40] 40) and
   16.14 +  AND  (infixr "&" 35) and
   16.15 +  OR  (infixr "|" 30) and
   16.16 +  IMPLIES  (infixr "-->" 25)
   16.17  
   16.18 -syntax (xsymbols output)
   16.19 -  "NOT"    ::"'a predicate => 'a predicate" ("\<not> _" [40] 40)
   16.20 -  "AND"    ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\<and>" 35)
   16.21 -  "OR"     ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\<or>" 30)
   16.22 -  "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\<longrightarrow>" 25)
   16.23 +notation (xsymbols output)
   16.24 +  NOT  ("\<not> _" [40] 40) and
   16.25 +  AND  (infixr "\<and>" 35) and
   16.26 +  OR  (infixr "\<or>" 30) and
   16.27 +  IMPLIES  (infixr "\<longrightarrow>" 25)
   16.28  
   16.29 -syntax (xsymbols)
   16.30 -  "satisfies"  ::"'a => 'a predicate => bool"    ("_ \<Turnstile> _" [100,9] 8)
   16.31 +notation (xsymbols)
   16.32 +  satisfies  ("_ \<Turnstile> _" [100,9] 8)
   16.33  
   16.34 -syntax (HTML output)
   16.35 -  "NOT"    ::"'a predicate => 'a predicate" ("\<not> _" [40] 40)
   16.36 -  "AND"    ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\<and>" 35)
   16.37 -  "OR"     ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\<or>" 30)
   16.38 +notation (HTML output)
   16.39 +  NOT  ("\<not> _" [40] 40) and
   16.40 +  AND  (infixr "\<and>" 35) and
   16.41 +  OR  (infixr "\<or>" 30)
   16.42  
   16.43  
   16.44  defs
    17.1 --- a/src/Sequents/LK0.thy	Wed Feb 24 22:04:10 2010 +0100
    17.2 +++ b/src/Sequents/LK0.thy	Wed Feb 24 22:09:50 2010 +0100
    17.3 @@ -43,23 +43,23 @@
    17.4    not_equal  (infixl "~=" 50) where
    17.5    "x ~= y == ~ (x = y)"
    17.6  
    17.7 -syntax (xsymbols)
    17.8 -  Not           :: "o => o"               ("\<not> _" [40] 40)
    17.9 -  conj          :: "[o, o] => o"          (infixr "\<and>" 35)
   17.10 -  disj          :: "[o, o] => o"          (infixr "\<or>" 30)
   17.11 -  imp           :: "[o, o] => o"          (infixr "\<longrightarrow>" 25)
   17.12 -  iff           :: "[o, o] => o"          (infixr "\<longleftrightarrow>" 25)
   17.13 -  All_binder    :: "[idts, o] => o"       ("(3\<forall>_./ _)" [0, 10] 10)
   17.14 -  Ex_binder     :: "[idts, o] => o"       ("(3\<exists>_./ _)" [0, 10] 10)
   17.15 -  not_equal     :: "['a, 'a] => o"        (infixl "\<noteq>" 50)
   17.16 +notation (xsymbols)
   17.17 +  Not  ("\<not> _" [40] 40) and
   17.18 +  conj  (infixr "\<and>" 35) and
   17.19 +  disj  (infixr "\<or>" 30) and
   17.20 +  imp  (infixr "\<longrightarrow>" 25) and
   17.21 +  iff  (infixr "\<longleftrightarrow>" 25) and
   17.22 +  All  (binder "\<forall>" 10) and
   17.23 +  Ex  (binder "\<exists>" 10) and
   17.24 +  not_equal  (infixl "\<noteq>" 50)
   17.25  
   17.26 -syntax (HTML output)
   17.27 -  Not           :: "o => o"               ("\<not> _" [40] 40)
   17.28 -  conj          :: "[o, o] => o"          (infixr "\<and>" 35)
   17.29 -  disj          :: "[o, o] => o"          (infixr "\<or>" 30)
   17.30 -  All_binder    :: "[idts, o] => o"       ("(3\<forall>_./ _)" [0, 10] 10)
   17.31 -  Ex_binder     :: "[idts, o] => o"       ("(3\<exists>_./ _)" [0, 10] 10)
   17.32 -  not_equal     :: "['a, 'a] => o"        (infixl "\<noteq>" 50)
   17.33 +notation (HTML output)
   17.34 +  Not  ("\<not> _" [40] 40) and
   17.35 +  conj  (infixr "\<and>" 35) and
   17.36 +  disj  (infixr "\<or>" 30) and
   17.37 +  All  (binder "\<forall>" 10) and
   17.38 +  Ex  (binder "\<exists>" 10) and
   17.39 +  not_equal  (infixl "\<noteq>" 50)
   17.40  
   17.41  local
   17.42