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/MicroJava/BV/BVExample.thy
changeset 15045 d59f7e2e18d3
parent 14045 a34d89ce6097
child 15570 8d8c70b41bab 
--- a/src/HOL/MicroJava/BV/BVExample.thy	Thu Jul 15 08:38:37 2004 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Thu Jul 15 13:11:34 2004 +0200
@@ -416,7 +416,7 @@
     in  kiljvm G mxs (1+size pTs+mxl) rT et instr start)"
 
 lemma [code]:
-  "unstables r step ss = (UN p:{..size ss(}. if \<not>stable r step ss p then {p} else {})"
+  "unstables r step ss = (UN p:{..<size ss}. if \<not>stable r step ss p then {p} else {})"
   apply (unfold unstables_def)
   apply (rule equalityI)
   apply (rule subsetI)
isabelle