# HG changeset patch
# User oheimb
# Date 891284594 -7200
# Node ID 02b86e36e98f97ac90f7830f810df1be6d9a8295
# Parent  329c09e15991215fe32d51071b37a5f8c6d9154d
removed superfluous translations

diff -r 329c09e15991 -r 02b86e36e98f src/HOL/IMP/Transition.thy
--- a/src/HOL/IMP/Transition.thy	Tue Mar 24 16:57:40 1998 +0100
+++ b/src/HOL/IMP/Transition.thy	Mon Mar 30 21:03:14 1998 +0200
@@ -17,12 +17,9 @@
 				("_ -*-> _" [81,81] 100)
 
 translations
-        "x -1-> (y,z)" == "(x,y,z) : evalc1" 
        	"cs0 -1-> cs1" == "(cs0,cs1) : evalc1"
-        "x -n-> (y,z)" == "(x,y,z) : evalc1 ^ n" 
-	"cs0 -n-> cs1" == "(cs0,cs1) : evalc1 ^ n"
-	"x -*-> (y,z)" == "(x,y,z) : evalc1 ^*" 
-	"cs0 -*-> cs1" == "(cs0,cs1) : evalc1 ^*"
+	"cs0 -n-> cs1" == "(cs0,cs1) : evalc1^n"
+	"cs0 -*-> cs1" == "(cs0,cs1) : evalc1^*"
 
 
 inductive evalc1