--- a/src/HOL/Proofs/Lambda/Lambda.thy Wed Dec 30 18:25:39 2015 +0100
+++ b/src/HOL/Proofs/Lambda/Lambda.thy Wed Dec 30 18:47:13 2015 +0100
@@ -64,11 +64,8 @@
| abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs s \<rightarrow>\<^sub>\<beta> Abs t"
abbreviation
- beta_reds :: "[dB, dB] => bool" (infixl "->>" 50) where
- "s ->> t == beta^** s t"
-
-notation (latex)
- beta_reds (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
+ beta_reds :: "[dB, dB] => bool" (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50) where
+ "s \<rightarrow>\<^sub>\<beta>\<^sup>* t == beta^** s t"
inductive_cases beta_cases [elim!]:
"Var i \<rightarrow>\<^sub>\<beta> t"
--- a/src/HOL/Proofs/Lambda/LambdaType.thy Wed Dec 30 18:25:39 2015 +0100
+++ b/src/HOL/Proofs/Lambda/LambdaType.thy Wed Dec 30 18:47:13 2015 +0100
@@ -55,18 +55,12 @@
abbreviation
typings_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
- ("_ ||- _ : _" [50, 50, 50] 50) where
- "env ||- ts : Ts == typings env ts Ts"
-
-notation (latex)
- typings_rel ("_ \<tturnstile> _ : _" [50, 50, 50] 50)
+ ("_ \<tturnstile> _ : _" [50, 50, 50] 50) where
+ "env \<tturnstile> ts : Ts == typings env ts Ts"
abbreviation
- funs :: "type list \<Rightarrow> type \<Rightarrow> type" (infixr "=>>" 200) where
- "Ts =>> T == foldr Fun Ts T"
-
-notation (latex)
- funs (infixr "\<Rrightarrow>" 200)
+ funs :: "type list \<Rightarrow> type \<Rightarrow> type" (infixr "\<Rrightarrow>" 200) where
+ "Ts \<Rrightarrow> T == foldr Fun Ts T"
subsection \<open>Some examples\<close>
--- a/src/HOL/Proofs/Lambda/ListBeta.thy Wed Dec 30 18:25:39 2015 +0100
+++ b/src/HOL/Proofs/Lambda/ListBeta.thy Wed Dec 30 18:47:13 2015 +0100
@@ -69,7 +69,7 @@
by (induct ss rule: rev_induct) auto
lemma apps_preserves_beta2 [simp]:
- "r ->> s ==> r \<degree>\<degree> ss ->> s \<degree>\<degree> ss"
+ "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> r \<degree>\<degree> ss \<rightarrow>\<^sub>\<beta>\<^sup>* s \<degree>\<degree> ss"
apply (induct set: rtranclp)
apply blast
apply (blast intro: apps_preserves_beta rtranclp.rtrancl_into_rtrancl)