diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Lambda/WeakNorm.thy
--- 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)