equal
deleted
inserted
replaced
387 Try $ (Repeat $ (Ca1 $ Free (assoc_calc (calc ,c), IDtype))) |
387 Try $ (Repeat $ (Ca1 $ Free (assoc_calc (calc ,c), IDtype))) |
388 | rule2stac _ (Rls_ rls) = |
388 | rule2stac _ (Rls_ rls) = |
389 Try $ (Rew_Set $ Free (id_rls rls, IDtype) $ HOLogic.false_const); |
389 Try $ (Rew_Set $ Free (id_rls rls, IDtype) $ HOLogic.false_const); |
390 (*val t = rule2stac [] (Thm ("real_diff_minus", num_str @{thm real_diff_minus)); |
390 (*val t = rule2stac [] (Thm ("real_diff_minus", num_str @{thm real_diff_minus)); |
391 atomt t; term2str t; |
391 atomt t; term2str t; |
392 val t = rule2stac calclist (Calc ("op +", eval_binop "#add_")); |
392 val t = rule2stac calclist (Calc ("Groups.plus_class.plus", eval_binop "#add_")); |
393 atomt t; term2str t; |
393 atomt t; term2str t; |
394 val t = rule2stac [] (Rls_ rearrange_assoc); |
394 val t = rule2stac [] (Rls_ rearrange_assoc); |
395 atomt t; term2str t; |
395 atomt t; term2str t; |
396 *) |
396 *) |
397 fun rule2stac_inst _ (Thm (thmID, _)) = |
397 fun rule2stac_inst _ (Thm (thmID, _)) = |
404 | rule2stac_inst _ (Rls_ rls) = |
404 | rule2stac_inst _ (Rls_ rls) = |
405 Try $ (Rew_Set_Inst $ Subs $ Free (id_rls rls, IDtype) $ |
405 Try $ (Rew_Set_Inst $ Subs $ Free (id_rls rls, IDtype) $ |
406 HOLogic.false_const); |
406 HOLogic.false_const); |
407 (*val t = rule2stac_inst [] (Thm ("real_diff_minus", num_str @{thm real_diff_minus)); |
407 (*val t = rule2stac_inst [] (Thm ("real_diff_minus", num_str @{thm real_diff_minus)); |
408 atomt t; term2str t; |
408 atomt t; term2str t; |
409 val t = rule2stac_inst calclist (Calc ("op +", eval_binop "#add_")); |
409 val t = rule2stac_inst calclist (Calc ("Groups.plus_class.plus", eval_binop "#add_")); |
410 atomt t; term2str t; |
410 atomt t; term2str t; |
411 val t = rule2stac_inst [] (Rls_ rearrange_assoc); |
411 val t = rule2stac_inst [] (Rls_ rearrange_assoc); |
412 atomt t; term2str t; |
412 atomt t; term2str t; |
413 *) |
413 *) |
414 |
414 |