diff -r 88d4c33d7947 -r 2a2c0dbeb4ac src/Tools/8bit/doc/Set2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/Set2.thy	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,9 @@
+consts
+	Ball	:: "'a set => ('a => bool) => bool"
+syntax
+	"@Ball"	:: "pttrn => 'a set => bool => bool"	("(3!_:_./ _)" 10)
+translations
+		"!x:A. P" == "Ball A (%x. P)"
+defs
+     Ball_def	"Ball A P == !x. x:A --> P x"
+