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/Abs_Int_ITP/Abs_Int2_ITP.thy
changeset 47818 151d137f1095
parent 47602 3d44790b5ab0
child 48480 cb03acfae211 
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy	Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy	Sat Apr 28 07:38:22 2012 +0200
@@ -202,7 +202,7 @@
     by (fastforce simp: Assign_le  map_acom_Assign intro: aval'_sound in_gamma_update
       split: option.splits del:subsetD)
 next
-  case Semi thus ?case apply (auto simp: Semi_le map_acom_Semi)
+  case Seq thus ?case apply (auto simp: Seq_le map_acom_Seq)
     by (metis le_post post_map_acom)
 next
   case (If b cs1 cs2 P)
isabelle