963 val rls = complete_square; |
963 val rls = complete_square; |
964 val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t; |
964 val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t; |
965 term2str t = "-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2"; |
965 term2str t = "-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2"; |
966 |
966 |
967 val thm = num_str @{thm square_explicit1}; |
967 val thm = num_str @{thm square_explicit1}; |
968 val SOME (t,asm) = rewrite_ thy dummy_ord Erls true thm t; |
968 val SOME (t,asm) = rewrite_ thy dummy_ord Rule_Set.Empty true thm t; |
969 term2str t = "(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8"; |
969 term2str t = "(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8"; |
970 |
970 |
971 val thm = num_str @{thm root_plus_minus}; |
971 val thm = num_str @{thm root_plus_minus}; |
972 val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t; |
972 val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t; |
973 term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^ |
973 term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^ |
974 "\n2 / 2 - x = -1 * sqrt ((2 / 2) ^^^ 2 - -8)"; |
974 "\n2 / 2 - x = -1 * sqrt ((2 / 2) ^^^ 2 - -8)"; |
975 |
975 |
976 (*the thm bdv_explicit2* here required to be constrained to ::real*) |
976 (*the thm bdv_explicit2* here required to be constrained to ::real*) |
977 val thm = num_str @{thm bdv_explicit2}; |
977 val thm = num_str @{thm bdv_explicit2}; |
978 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Erls true inst thm t; |
978 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t; |
979 term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^ |
979 term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^ |
980 "\n-1 * x = - (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8)"; |
980 "\n-1 * x = - (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8)"; |
981 |
981 |
982 val thm = num_str @{thm bdv_explicit3}; |
982 val thm = num_str @{thm bdv_explicit3}; |
983 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Erls true inst thm t; |
983 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t; |
984 term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^ |
984 term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^ |
985 "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))"; |
985 "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))"; |
986 |
986 |
987 val thm = num_str @{thm bdv_explicit2}; |
987 val thm = num_str @{thm bdv_explicit2}; |
988 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Erls true inst thm t; |
988 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t; |
989 term2str t = "-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |"^ |
989 term2str t = "-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |"^ |
990 "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))"; |
990 "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))"; |
991 |
991 |
992 val rls = calculate_RootRat; |
992 val rls = calculate_RootRat; |
993 val SOME (t,asm) = rewrite_set_ thy true rls t; |
993 val SOME (t,asm) = rewrite_set_ thy true rls t; |