equal
deleted
inserted
replaced
372 val t = TermC.str2term "x \<up> 2 * x"; |
372 val t = TermC.str2term "x \<up> 2 * x"; |
373 |
373 |
374 if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2"; |
374 if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2"; |
375 val tm = TermC.str2term "(x \<up> 2 * x) is_multUnordered"; |
375 val tm = TermC.str2term "(x \<up> 2 * x) is_multUnordered"; |
376 |
376 |
377 (*+*)case eval_is_multUnordered "testid" "" tm thy of |
377 (*+*)case eval_is_multUnordered "testid" "" tm ctxt of |
378 (*+*) SOME |
378 (*+*) SOME |
379 (*+*) ("testidx \<up> 2 * x_", |
379 (*+*) ("testidx \<up> 2 * x_", |
380 (*+*) Const (\<^const_name>\<open>Trueprop\<close>, _) $ |
380 (*+*) Const (\<^const_name>\<open>Trueprop\<close>, _) $ |
381 (*+*) (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ |
381 (*+*) (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ |
382 (*+*) (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ |
382 (*+*) (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ |
385 (*+*) Const (\<^const_name>\<open>True\<close>, _))) => () |
385 (*+*) Const (\<^const_name>\<open>True\<close>, _))) => () |
386 (*+*)(* ^^^^^^ compare ---vvv *) |
386 (*+*)(* ^^^^^^ compare ---vvv *) |
387 (*+*)| _ => error "rewrite.sml diff. eval_is_multUnordered 2b CHANGED"; |
387 (*+*)| _ => error "rewrite.sml diff. eval_is_multUnordered 2b CHANGED"; |
388 |
388 |
389 |
389 |
390 eval_is_multUnordered "testid" "" tm thy; |
390 eval_is_multUnordered "testid" "" tm ctxt; |
391 |
391 |
392 case eval_is_multUnordered "testid" "" tm thy of |
392 case eval_is_multUnordered "testid" "" tm ctxt of |
393 SOME (_, Const (\<^const_name>\<open>Trueprop\<close>, _) $ |
393 SOME (_, Const (\<^const_name>\<open>Trueprop\<close>, _) $ |
394 (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ |
394 (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ |
395 (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ _) $ |
395 (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ _) $ |
396 Const (\<^const_name>\<open>True\<close>, _))) => () |
396 Const (\<^const_name>\<open>True\<close>, _))) => () |
397 | _ => error "rewrite.sml diff. eval_is_multUnordered 2b"; |
397 | _ => error "rewrite.sml diff. eval_is_multUnordered 2b"; |