Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removed superfluous translations
authoroheimb
Mon, 30 Mar 1998 21:03:14 +0200
changeset 4757 02b86e36e98f
parent 4756 329c09e15991
child 4758 35f4ad4f055d
removed superfluous translations
src/HOL/IMP/Transition.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle