src/ZF/IMP/Evalb0.thy

--- a/src/ZF/IMP/Evalb0.thy	Sat Apr 05 16:18:58 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(*  Title: 	ZF/IMP/Evalb0.thy
-    ID:         $Id$
-    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
-    Copyright   1994 TUM
-*)
-
-Evalb0 = Evala + Bexp +
-
-consts 
-        evalb	 :: "i"	
-        "@evalb" :: "[i,i,i] => o"	("<_,_>/ -b-> _")
-
-translations
-	"<be,sig> -b-> b" == "<be,sig,b> : evalb"
-end