src/HOL/MicroJava/J/JBasis.thy

--- a/src/HOL/MicroJava/J/JBasis.thy	Mon Jan 10 16:06:43 2000 +0100
+++ b/src/HOL/MicroJava/J/JBasis.thy	Mon Jan 10 16:07:29 2000 +0100
@@ -13,7 +13,4 @@
   unique  :: "('a \\<times> 'b) list \\<Rightarrow> bool"
  "unique  \\<equiv> nodups \\<circ> map fst"
 
-  list_all2 :: "('a \\<Rightarrow> 'b \\<Rightarrow> bool) \\<Rightarrow> ('a list \\<Rightarrow> 'b list \\<Rightarrow> bool)"
- "list_all2 P xs ys \\<equiv> length xs = length ys \\<and> (\\<forall> (x,y)\\<in>set (zip xs ys). P x y)"
-
 end