# HG changeset patch
# User wenzelm
# Date 1451496276 -3600
# Node ID a63a11b0933591f5867ffe3ec3fba8ac5f22a8e0
# Parent  cdea44c775fa7177b33d54224eb34cf32708f123
clarified print modes;

diff -r cdea44c775fa -r a63a11b09335 src/HOL/Proofs/Lambda/Eta.thy
--- a/src/HOL/Proofs/Lambda/Eta.thy	Wed Dec 30 18:17:28 2015 +0100
+++ b/src/HOL/Proofs/Lambda/Eta.thy	Wed Dec 30 18:24:36 2015 +0100
@@ -26,16 +26,12 @@
   | abs [simp, intro]: "s \<rightarrow>\<^sub>\<eta> t ==> Abs s \<rightarrow>\<^sub>\<eta> Abs t"
 
 abbreviation
-  eta_reds :: "[dB, dB] => bool"   (infixl "-e>>" 50) where
-  "s -e>> t == eta^** s t"
+  eta_reds :: "[dB, dB] => bool"   (infixl "\<rightarrow>\<^sub>\<eta>\<^sup>*" 50) where
+  "s \<rightarrow>\<^sub>\<eta>\<^sup>* t == eta^** s t"
 
 abbreviation
-  eta_red0 :: "[dB, dB] => bool"   (infixl "-e>=" 50) where
-  "s -e>= t == eta^== s t"
-
-notation (xsymbols)
-  eta_reds  (infixl "\<rightarrow>\<^sub>\<eta>\<^sup>*" 50) and
-  eta_red0  (infixl "\<rightarrow>\<^sub>\<eta>\<^sup>=" 50)
+  eta_red0 :: "[dB, dB] => bool"   (infixl "\<rightarrow>\<^sub>\<eta>\<^sup>=" 50) where
+  "s \<rightarrow>\<^sub>\<eta>\<^sup>= t == eta^== s t"
 
 inductive_cases eta_cases [elim!]:
   "Abs s \<rightarrow>\<^sub>\<eta> z"
diff -r cdea44c775fa -r a63a11b09335 src/HOL/Proofs/Lambda/LambdaType.thy
--- a/src/HOL/Proofs/Lambda/LambdaType.thy	Wed Dec 30 18:17:28 2015 +0100
+++ b/src/HOL/Proofs/Lambda/LambdaType.thy	Wed Dec 30 18:24:36 2015 +0100
@@ -11,11 +11,8 @@
 subsection {* Environments *}
 
 definition
-  shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"  ("_<_:_>" [90, 0, 0] 91) where
-  "e<i:a> = (\<lambda>j. if j < i then e j else if j = i then a else e (j - 1))"
-
-notation (xsymbols)
-  shift  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
+  shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91) where
+  "e\<langle>i:a\<rangle> = (\<lambda>j. if j < i then e j else if j = i then a else e (j - 1))"
 
 lemma shift_eq [simp]: "i = j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = T"
   by (simp add: shift_def)