5500 "problem3 = A (And (Le (Sub (Floor (Bound 0)) (Bound 0))) (Le (Add (Bound 0) (Floor (Neg (Bound 0))))))" |
5500 "problem3 = A (And (Le (Sub (Floor (Bound 0)) (Bound 0))) (Le (Add (Bound 0) (Floor (Neg (Bound 0))))))" |
5501 |
5501 |
5502 definition |
5502 definition |
5503 "problem4 = E (And (Ge (Sub (Bound 1) (Bound 0))) (Eq (Add (Floor (Bound 1)) (Floor (Neg (Bound 0))))))" |
5503 "problem4 = E (And (Ge (Sub (Bound 1) (Bound 0))) (Eq (Add (Floor (Bound 1)) (Floor (Neg (Bound 0))))))" |
5504 |
5504 |
5505 ML {* @{code mircfrqe} @{code problem1} *} |
5505 ML {* |
5506 ML {* @{code mirlfrqe} @{code problem1} *} |
5506 Par_List.map (fn e => e ()) |
5507 ML {* @{code mircfrqe} @{code problem2} *} |
5507 [fn () => @{code mircfrqe} @{code problem1}, |
5508 ML {* @{code mirlfrqe} @{code problem2} *} |
5508 fn () => @{code mirlfrqe} @{code problem1}, |
5509 ML {* @{code mircfrqe} @{code problem3} *} |
5509 fn () => @{code mircfrqe} @{code problem2}, |
5510 ML {* @{code mirlfrqe} @{code problem3} *} |
5510 fn () => @{code mirlfrqe} @{code problem2}, |
5511 ML {* @{code mircfrqe} @{code problem4} *} |
5511 fn () => @{code mircfrqe} @{code problem3}, |
5512 ML {* @{code mirlfrqe} @{code problem4} *} |
5512 fn () => @{code mirlfrqe} @{code problem3}, |
|
5513 fn () => @{code mircfrqe} @{code problem4}, |
|
5514 fn () => @{code mirlfrqe} @{code problem4}] |
|
5515 *} |
5513 |
5516 |
5514 (*code_reflect Mir |
5517 (*code_reflect Mir |
5515 functions mircfrqe mirlfrqe |
5518 functions mircfrqe mirlfrqe |
5516 file "mir.ML"*) |
5519 file "mir.ML"*) |
5517 |
5520 |