src/HOL/MicroJava/BV/JVMType.thy
changeset 61943 7fba644ed827
parent 61361 8b5f00202e1a
child 61952 546958347e05
     1.1 --- a/src/HOL/MicroJava/BV/JVMType.thy	Sun Dec 27 21:46:36 2015 +0100
     1.2 +++ b/src/HOL/MicroJava/BV/JVMType.thy	Sun Dec 27 22:07:17 2015 +0100
     1.3 @@ -62,7 +62,7 @@
     1.4                     
     1.5  
     1.6  lemma JVM_states_unfold: 
     1.7 -  "states S maxs maxr == err(opt((Union {list n (types S) |n. n <= maxs}) <*>
     1.8 +  "states S maxs maxr == err(opt((Union {list n (types S) |n. n <= maxs}) \<times>
     1.9                                    list maxr (err(types S))))"
    1.10    apply (unfold states_def sl_def Opt.esl_def Err.sl_def
    1.11           stk_esl_def reg_sl_def Product.esl_def