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/Bali/DefiniteAssignmentCorrect.thy
changeset 18447 da548623916a
parent 18249 4398f0f12579
child 18459 2b102759160d 
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Wed Dec 21 12:02:57 2005 +0100
@@ -3381,7 +3381,7 @@
         proof -
           from normal_s3 s3
           have "normal (x1,s1)"
-            by (cases s2) (simp add: abrupt_if_def)
+            by (cases s2) (simp add: abrupt_if_def not_Some_eq)
           with normal_s3 nrmAss_C1 s3 s1_s2
           show ?thesis
             by fastsimp
isabelle