equal
deleted
inserted
replaced
21 lin_isolate_add1: "(a + b*bdv = 0) = (b*bdv = (-1)*a)" and |
21 lin_isolate_add1: "(a + b*bdv = 0) = (b*bdv = (-1)*a)" and |
22 lin_isolate_add2: "(a + bdv = 0) = ( bdv = (-1)*a)" and |
22 lin_isolate_add2: "(a + bdv = 0) = ( bdv = (-1)*a)" and |
23 lin_isolate_div: "[|Not(b=0)|] ==> (b*bdv = c) = (bdv = c / b)" |
23 lin_isolate_div: "[|Not(b=0)|] ==> (b*bdv = c) = (bdv = c / b)" |
24 |
24 |
25 ML \<open> |
25 ML \<open> |
26 val thy = @{theory}; |
|
27 |
|
28 val LinEq_prls = (*3.10.02:just the following order due to subterm evaluation*) |
26 val LinEq_prls = (*3.10.02:just the following order due to subterm evaluation*) |
29 Rule_Set.append_rules "LinEq_prls" Rule_Set.empty |
27 Rule_Set.append_rules "LinEq_prls" Rule_Set.empty |
30 [Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"), |
28 [Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"), |
31 Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches ""), |
29 Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches ""), |
32 Rule.Eval ("Prog_Expr.lhs" , Prog_Expr.eval_lhs ""), |
30 Rule.Eval ("Prog_Expr.lhs" , Prog_Expr.eval_lhs ""), |