src/ZF/IMP/Evala0.thy
changeset 13895 b6105462ccd3
parent 13894 8018173a7979
child 13896 717bd79b976f
--- a/src/ZF/IMP/Evala0.thy	Sat Apr 05 16:18:58 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-(*  Title: 	ZF/IMP/Evala0.thy
-    ID:         $Id$
-    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
-    Copyright   1994 TUM
-*)
-
-Evala0 = Aexp +
-
-consts  evala    :: "i"
-       "@evala"  :: "[i,i,i] => o"	("<_,_>/ -a-> _")
-
-translations
- "<ae,sig> -a-> n" == "<ae,sig,n> : evala"
-end