# HG changeset patch
# User wenzelm
# Date 1451497633 -3600
# Node ID 305baa3fc2207e53480cb33c27f1f42fefe8217f
# Parent  2461779da2b8d0ac75d92994a6ccff1e08360563
clarified print modes;
more symbols;

diff -r 2461779da2b8 -r 305baa3fc220 src/HOL/Proofs/Lambda/Lambda.thy
--- 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"
diff -r 2461779da2b8 -r 305baa3fc220 src/HOL/Proofs/Lambda/LambdaType.thy
--- 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>
diff -r 2461779da2b8 -r 305baa3fc220 src/HOL/Proofs/Lambda/ListBeta.thy
--- 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)