--- 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"
--- 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)