404 "#eval_occur_exactly_in_") |
404 "#eval_occur_exactly_in_") |
405 ], |
405 ], |
406 scr = EmptyScr}; |
406 scr = EmptyScr}; |
407 *} |
407 *} |
408 |
408 |
409 ML {* |
|
410 ruleset' := |
|
411 overwritelthy @{theory} |
|
412 (!ruleset', |
|
413 [("simplify_System_parenthesized", prep_rls simplify_System_parenthesized), |
|
414 ("simplify_System", prep_rls simplify_System), |
|
415 ("isolate_bdvs", prep_rls isolate_bdvs), |
|
416 ("isolate_bdvs_4x4", prep_rls isolate_bdvs_4x4), |
|
417 ("order_system", prep_rls order_system), |
|
418 ("order_add_mult_System", prep_rls order_add_mult_System), |
|
419 ("norm_System_noadd_fractions", prep_rls norm_System_noadd_fractions), |
|
420 ("norm_System", prep_rls norm_System) |
|
421 ]); |
|
422 *} |
|
423 setup {* KEStore_Elems.add_rlss |
409 setup {* KEStore_Elems.add_rlss |
424 [("simplify_System_parenthesized", |
410 [("simplify_System_parenthesized", |
425 (Context.theory_name @{theory}, prep_rls simplify_System_parenthesized)), |
411 (Context.theory_name @{theory}, prep_rls simplify_System_parenthesized)), |
426 ("simplify_System", (Context.theory_name @{theory}, prep_rls simplify_System)), |
412 ("simplify_System", (Context.theory_name @{theory}, prep_rls simplify_System)), |
427 ("isolate_bdvs", (Context.theory_name @{theory}, prep_rls isolate_bdvs)), |
413 ("isolate_bdvs", (Context.theory_name @{theory}, prep_rls isolate_bdvs)), |