src/Tools/isac/Knowledge/Rational.thy
changeset 60320 02102eaa2021
parent 60319 2edbed71fde6
child 60331 40eb8aa2b0d6
     1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Mon Jul 12 17:21:37 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Tue Jul 13 08:52:35 2021 +0200
     1.3 @@ -406,7 +406,8 @@
     1.4      (Rule_Def.Repeat {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), 
     1.5        erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
     1.6        rules = 
     1.7 -        [Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
     1.8 +       [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_"),
     1.9 +        Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
    1.10          Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),
    1.11          Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
    1.12          Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false})],