--- a/src/HOL/Induct/LFilter.thy Wed Jul 11 11:13:08 2007 +0200
+++ b/src/HOL/Induct/LFilter.thy Wed Jul 11 11:14:51 2007 +0200
@@ -9,13 +9,12 @@
theory LFilter imports LList begin
-consts
+inductive_set
findRel :: "('a => bool) => ('a llist * 'a llist)set"
-
-inductive "findRel p"
- intros
+ for p :: "'a => bool"
+ where
found: "p x ==> (LCons x l, LCons x l) \<in> findRel p"
- seek: "[| ~p x; (l,l') \<in> findRel p |] ==> (LCons x l, l') \<in> findRel p"
+ | seek: "[| ~p x; (l,l') \<in> findRel p |] ==> (LCons x l, l') \<in> findRel p"
declare findRel.intros [intro]