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})],