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/HOL/IMP/Comp_Rev.thy
changeset 47818 151d137f1095
parent 45605 a89b4bc311a5
child 50060 43753eca324a 
--- a/src/HOL/IMP/Comp_Rev.thy	Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Comp_Rev.thy	Sat Apr 28 07:38:22 2012 +0200
@@ -224,10 +224,10 @@
 next
   case Assign thus ?case by simp
 next
-  case (Semi c1 c2)
-  from Semi.prems
+  case (Seq c1 c2)
+  from Seq.prems
   show ?case 
-    by (fastforce dest: Semi.IH [THEN subsetD])
+    by (fastforce dest: Seq.IH [THEN subsetD])
 next
   case (If b c1 c2)
   from If.prems
@@ -492,7 +492,7 @@
   thus ?case
     by simp (fastforce dest!: exec_n_split_full simp: exec_n_simps)
 next
-  case (Semi c1 c2)
+  case (Seq c1 c2)
   thus ?case by (fastforce dest!: exec_n_split_full)
 next
   case (If b c1 c2)
isabelle