402 Rule.Thm ("or_false",TermC.num_str @{thm or_false}), |
402 Rule.Thm ("or_false",TermC.num_str @{thm or_false}), |
403 Rule.Thm ("and_commute",TermC.num_str @{thm and_commute}), |
403 Rule.Thm ("and_commute",TermC.num_str @{thm and_commute}), |
404 Rule.Thm ("or_commute",TermC.num_str @{thm or_commute}), |
404 Rule.Thm ("or_commute",TermC.num_str @{thm or_commute}), |
405 |
405 |
406 Rule.Calc ("Atools.is'_const",eval_const "#is_const_"), |
406 Rule.Calc ("Atools.is'_const",eval_const "#is_const_"), |
407 Rule.Calc ("Tools.matches",eval_matches ""), |
407 Rule.Calc ("Tools.matches", Tools.eval_matches ""), |
408 |
408 |
409 Rule.Calc ("Groups.plus_class.plus",eval_binop "#add_"), |
409 Rule.Calc ("Groups.plus_class.plus",eval_binop "#add_"), |
410 Rule.Calc ("Groups.times_class.times",eval_binop "#mult_"), |
410 Rule.Calc ("Groups.times_class.times",eval_binop "#mult_"), |
411 Rule.Calc ("Atools.pow" ,eval_binop "#power_"), |
411 Rule.Calc ("Atools.pow" ,eval_binop "#power_"), |
412 |
412 |
444 Rule.Thm ("root_ge0_1",TermC.num_str @{thm root_ge0_1}), |
444 Rule.Thm ("root_ge0_1",TermC.num_str @{thm root_ge0_1}), |
445 Rule.Thm ("root_ge0_2",TermC.num_str @{thm root_ge0_2}), |
445 Rule.Thm ("root_ge0_2",TermC.num_str @{thm root_ge0_2}), |
446 |
446 |
447 Rule.Calc ("Atools.is'_const",eval_const "#is_const_"), |
447 Rule.Calc ("Atools.is'_const",eval_const "#is_const_"), |
448 Rule.Calc ("Test.contains'_root",eval_contains_root "#eval_contains_root"), |
448 Rule.Calc ("Test.contains'_root",eval_contains_root "#eval_contains_root"), |
449 Rule.Calc ("Tools.matches",eval_matches ""), |
449 Rule.Calc ("Tools.matches", Tools.eval_matches ""), |
450 Rule.Calc ("Test.contains'_root", |
450 Rule.Calc ("Test.contains'_root", |
451 eval_contains_root"#contains_root_"), |
451 eval_contains_root"#contains_root_"), |
452 |
452 |
453 Rule.Calc ("Groups.plus_class.plus",eval_binop "#add_"), |
453 Rule.Calc ("Groups.plus_class.plus",eval_binop "#add_"), |
454 Rule.Calc ("Groups.times_class.times",eval_binop "#mult_"), |
454 Rule.Calc ("Groups.times_class.times",eval_binop "#mult_"), |
591 [("Test_simplify", (Context.theory_name @{theory}, prep_rls' Test_simplify)), |
591 [("Test_simplify", (Context.theory_name @{theory}, prep_rls' Test_simplify)), |
592 ("tval_rls", (Context.theory_name @{theory}, prep_rls' tval_rls)), |
592 ("tval_rls", (Context.theory_name @{theory}, prep_rls' tval_rls)), |
593 ("isolate_root", (Context.theory_name @{theory}, prep_rls' isolate_root)), |
593 ("isolate_root", (Context.theory_name @{theory}, prep_rls' isolate_root)), |
594 ("isolate_bdv", (Context.theory_name @{theory}, prep_rls' isolate_bdv)), |
594 ("isolate_bdv", (Context.theory_name @{theory}, prep_rls' isolate_bdv)), |
595 ("matches", (Context.theory_name @{theory}, prep_rls' |
595 ("matches", (Context.theory_name @{theory}, prep_rls' |
596 (Rule.append_rls "matches" testerls [Rule.Calc ("Tools.matches",eval_matches "#matches_")])))] |
596 (Rule.append_rls "matches" testerls [Rule.Calc ("Tools.matches", Tools.eval_matches "#matches_")])))] |
597 \<close> |
597 \<close> |
598 |
598 |
599 subsection \<open>problems\<close> |
599 subsection \<open>problems\<close> |
600 (** problem types **) |
600 (** problem types **) |
601 setup \<open>KEStore_Elems.add_pbts |
601 setup \<open>KEStore_Elems.add_pbts |