equal
deleted
inserted
replaced
22 (_))" 9) |
22 (_))" 9) |
23 (*-------------------- rules------------------------------------------------*) |
23 (*-------------------- rules------------------------------------------------*) |
24 |
24 |
25 axioms |
25 axioms |
26 (* eliminate ratRootTerm *) |
26 (* eliminate ratRootTerm *) |
27 rootrat_equation_left_1 |
27 rootrat_equation_left_1: |
28 "[|c is_rootTerm_in bdv|] ==> ( (a + b/c = d) = ( b = (d - a) * c ))" |
28 "[|c is_rootTerm_in bdv|] ==> ( (a + b/c = d) = ( b = (d - a) * c ))" |
29 rootrat_equation_left_2 |
29 rootrat_equation_left_2: |
30 "[|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c ))" |
30 "[|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c ))" |
31 rootrat_equation_right_2 |
31 rootrat_equation_right_2: |
32 "[|f is_rootTerm_in bdv|] ==> ( (a = d + e/f) = ( (a - d) * f = e ))" |
32 "[|f is_rootTerm_in bdv|] ==> ( (a = d + e/f) = ( (a - d) * f = e ))" |
33 rootrat_equation_right_1 |
33 rootrat_equation_right_1: |
34 "[|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))" |
34 "[|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))" |
35 |
35 |
36 ML {* |
36 ML {* |
37 val thy = @{theory}; |
37 val thy = @{theory}; |
38 |
38 |