src/HOL/IMP/Transition.thy
changeset 1789 aade046ec6d5
parent 1701 a26fbeaaaabd
child 4757 02b86e36e98f
     1.1 --- a/src/HOL/IMP/Transition.thy	Thu Jun 06 13:13:18 1996 +0200
     1.2 +++ b/src/HOL/IMP/Transition.thy	Thu Jun 06 14:39:44 1996 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4  	"cs0 -*-> cs1" == "(cs0,cs1) : evalc1 ^*"
     1.5  
     1.6  
     1.7 -inductive "evalc1"
     1.8 +inductive evalc1
     1.9    intrs
    1.10      Assign "(x := a,s) -1-> (SKIP,s[a s / x])"
    1.11