335 (*Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""), *) |
335 (*Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""), *) |
336 (*Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),*) |
336 (*Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),*) |
337 Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"), |
337 Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"), |
338 Rule.Eval ("RootEq.is_rootTerm_in", eval_is_rootTerm_in ""), |
338 Rule.Eval ("RootEq.is_rootTerm_in", eval_is_rootTerm_in ""), |
339 Rule.Eval ("RatEq.is_ratequation_in", eval_is_ratequation_in ""), |
339 Rule.Eval ("RatEq.is_ratequation_in", eval_is_ratequation_in ""), |
340 Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}), |
340 Rule.Thm ("not_true", @{thm not_true}), |
341 Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}), |
341 Rule.Thm ("not_false", @{thm not_false}), |
342 Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}), |
342 Rule.Thm ("and_true", @{thm and_true}), |
343 Rule.Thm ("and_false",ThmC.numerals_to_Free @{thm and_false}), |
343 Rule.Thm ("and_false", @{thm and_false}), |
344 Rule.Thm ("or_true",ThmC.numerals_to_Free @{thm or_true}), |
344 Rule.Thm ("or_true", @{thm or_true}), |
345 Rule.Thm ("or_false",ThmC.numerals_to_Free @{thm or_false}) |
345 Rule.Thm ("or_false", @{thm or_false}) |
346 ]; |
346 ]; |
347 |
347 |
348 val PolyEq_erls = |
348 val PolyEq_erls = |
349 Rule_Set.merge "PolyEq_erls" LinEq_erls |
349 Rule_Set.merge "PolyEq_erls" LinEq_erls |
350 (Rule_Set.append_rules "ops_preds" calculate_Rational |
350 (Rule_Set.append_rules "ops_preds" calculate_Rational |