src/Tools/8bit/doc/Set2_a.thy
changeset 11390 735bf767833a
parent 11389 55e2aef8909b
child 11391 e8638d07fdee
--- a/src/Tools/8bit/doc/Set2_a.thy	Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-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"
-