equal
deleted
inserted
replaced
852 val t = TermC.str2term "1 < 2"; |
852 val t = TermC.str2term "1 < 2"; |
853 val SOME (t',_) = rewrite_set_ ctxt false powers_erls t; UnparseC.term t'; |
853 val SOME (t',_) = rewrite_set_ ctxt false powers_erls t; UnparseC.term t'; |
854 "HOL.True"; |
854 "HOL.True"; |
855 |
855 |
856 val t = TermC.str2term "(6*x) \<up> 2"; |
856 val t = TermC.str2term "(6*x) \<up> 2"; |
857 val SOME (t',_) = rewrite_ ctxt dummy_ord powers_erls false @{thm realpow_def_atom} t; |
857 val SOME (t',_) = rewrite_ ctxt Rewrite_Ord.function_empty powers_erls false @{thm realpow_def_atom} t; |
858 if UnparseC.term t' = "6 * x * (6 * x) \<up> (2 + - 1)" then () |
858 if UnparseC.term t' = "6 * x * (6 * x) \<up> (2 + - 1)" then () |
859 else error "rational.sml powers_erls (6*x) \<up> 2"; |
859 else error "rational.sml powers_erls (6*x) \<up> 2"; |
860 |
860 |
861 val t = TermC.str2term "- 1 * (- 2 * (5 / 2 * (13 * x / 2)))"; |
861 val t = TermC.str2term "- 1 * (- 2 * (5 / 2 * (13 * x / 2)))"; |
862 val SOME (t',_) = rewrite_set_ ctxt false norm_Rational t; UnparseC.term t'; |
862 val SOME (t',_) = rewrite_set_ ctxt false norm_Rational t; UnparseC.term t'; |