src/HOL/Statespace/StateSpaceEx.thy

--- a/src/HOL/Statespace/StateSpaceEx.thy	Thu Oct 16 17:07:20 2008 +0200
+++ b/src/HOL/Statespace/StateSpaceEx.thy	Thu Oct 16 17:19:47 2008 +0200
@@ -201,10 +201,12 @@
 implemented correctly in future Isabelle versions. *}
 
 lemma 
- includes foo
- shows True
+  assumes "foo f a b c p1 i1 p2 i2 p3 i3 p4 i4"
+  shows True
+proof
+  interpret foo [f a b c p1 i1 p2 i2 p3 i3 p4 i4] by fact
   term "s<a := i>\<cdot>a = i"
-  by simp
+qed
 
 (*
 lemma