# HG changeset patch
# User berghofe
# Date 1178805119 -7200
# Node ID 86b4a7d04d43f5e6d2776198af68ba7e534eadaf
# Parent  17f1d7af43bd2da5576b9b2a13d52a90588b12a6
Moved extraction_expand declaration of listall_def outside of definition.

diff -r 17f1d7af43bd -r 86b4a7d04d43 src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Thu May 10 15:50:56 2007 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy	Thu May 10 15:51:59 2007 +0200
@@ -20,7 +20,9 @@
 
 definition
   listall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
-  [extraction_expand]: "listall P xs \<equiv> (\<forall>i. i < length xs \<longrightarrow> P (xs ! i))"
+  "listall P xs \<equiv> (\<forall>i. i < length xs \<longrightarrow> P (xs ! i))"
+
+declare listall_def [extraction_expand]
 
 theorem listall_nil: "listall P []"
   by (simp add: listall_def)