Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/IMP/Com.thy
changeset 518 4530c45370b4
parent 514 ab2c867829ec
child 653 6eeff82979df 
--- a/src/ZF/IMP/Com.thy	Fri Aug 12 18:45:33 1994 +0200
+++ b/src/ZF/IMP/Com.thy	Mon Aug 15 16:12:35 1994 +0200
@@ -109,10 +109,12 @@
     semi    "[| <c0,sigma> -c-> sigma2; <c1,sigma2> -c-> sigma1 |] ==> \
 \            <c0 ; c1, sigma> -c-> sigma1"
 
-    ifc1     "[| c1: com; <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] ==> \
+    ifc1     "[| b:bexp; c1:com; sigma:loc->nat;   \
+\		 <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] ==> \
 \             <ifc b then c0 else c1, sigma> -c-> sigma1"
 
-    ifc0     "[| c0 : com; <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |] ==> \
+    ifc0     "[| b:bexp; c0:com; sigma:loc->nat;   \
+\		 <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |] ==> \
 \             <ifc b then c0 else c1, sigma> -c-> sigma1"
 
     while0   "[| c: com; <b, sigma> -b-> 0 |] ==> \
isabelle