equal
deleted
inserted
replaced
13 |
13 |
14 "----------- val rls = calculate_RootRat > calculate_Rational ----"; |
14 "----------- val rls = calculate_RootRat > calculate_Rational ----"; |
15 "----------- val rls = calculate_RootRat > calculate_Rational ----"; |
15 "----------- val rls = calculate_RootRat > calculate_Rational ----"; |
16 "----------- val rls = calculate_RootRat > calculate_Rational ----"; |
16 "----------- val rls = calculate_RootRat > calculate_Rational ----"; |
17 (*val calculate_RootRat = |
17 (*val calculate_RootRat = |
18 append_rls "calculate_RootRat" calculate_Rational [...] |
18 Rule_Set.append_rules "calculate_RootRat" calculate_Rational [...] |
19 val calculate_Rational = prep_rls (merge_rls "calculate_Rational" [...] |
19 val calculate_Rational = prep_rls (merge_rls "calculate_Rational" [...] |
20 calculate_Poly |
20 calculate_Poly |
21 val calculate_Poly = |
21 val calculate_Poly = |
22 append_rls "calculate_PolyFIXXXME.not.impl." e_rls []; |
22 Rule_Set.append_rules "calculate_PolyFIXXXME.not.impl." Rule_Set.empty []; |
23 WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat |
23 WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat |
24 *) |
24 *) |
25 |
25 |
26 val thy = @{theory RootRat}; |
26 val thy = @{theory RootRat}; |
27 val ctxt = Proof_Context.init_global thy; |
27 val ctxt = Proof_Context.init_global thy; |
30 atomty t; (*!real ?by sqrt and ^^^?*) |
30 atomty t; (*!real ?by sqrt and ^^^?*) |
31 |
31 |
32 "--- val rls = calculate_Poly ---"; |
32 "--- val rls = calculate_Poly ---"; |
33 (*val rls = assoc_rls "calculate_Poly"; WAS ME_Isa: 'calculate_Poly' not in system |
33 (*val rls = assoc_rls "calculate_Poly"; WAS ME_Isa: 'calculate_Poly' not in system |
34 goon with what just started ...*) |
34 goon with what just started ...*) |
35 val calculate_Poly = append_rls "calculate_Poly" e_rls |
35 val calculate_Poly = Rule_Set.append_rules "calculate_Poly" Rule_Set.empty |
36 [ Num_Calc ("Groups.plus_class.plus",eval_binop "#add_"), |
36 [ Num_Calc ("Groups.plus_class.plus",eval_binop "#add_"), |
37 Num_Calc ("Groups.minus_class.minus",eval_binop "#sub_"), |
37 Num_Calc ("Groups.minus_class.minus",eval_binop "#sub_"), |
38 Num_Calc ("Groups.times_class.times",eval_binop "#mult_"), |
38 Num_Calc ("Groups.times_class.times",eval_binop "#mult_"), |
39 Num_Calc ("Prog_Expr.pow" ,eval_binop "#power_") |
39 Num_Calc ("Prog_Expr.pow" ,eval_binop "#power_") |
40 ]; |
40 ]; |