--- a/src/HOL/Lambda/WeakNorm.thy Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Lambda/WeakNorm.thy Fri Nov 17 02:20:03 2006 +0100
@@ -17,7 +17,7 @@
subsection {* Terms in normal form *}
definition
- listall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
+ listall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
"listall P xs == (\<forall>i. i < length xs \<longrightarrow> P (xs ! i))"
declare listall_def [extraction_expand]
@@ -362,7 +362,7 @@
rtyping :: "((nat \<Rightarrow> type) \<times> dB \<times> type) set"
abbreviation
- rtyping_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ |-\<^sub>R _ : _" [50, 50, 50] 50)
+ rtyping_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ |-\<^sub>R _ : _" [50, 50, 50] 50) where
"e |-\<^sub>R t : T == (e, t, T) \<in> rtyping"
notation (xsymbols)