equal
deleted
inserted
replaced
124 ( *//----------------- dropped with "purge code for theory-hierarchy" *) |
124 ( *//----------------- dropped with "purge code for theory-hierarchy" *) |
125 |
125 |
126 "----------- fun is_contained_in ------------------------"; |
126 "----------- fun is_contained_in ------------------------"; |
127 "----------- fun is_contained_in ------------------------"; |
127 "----------- fun is_contained_in ------------------------"; |
128 "----------- fun is_contained_in ------------------------"; |
128 "----------- fun is_contained_in ------------------------"; |
129 val r1 = Thm ("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus}); |
129 val r1 = Thm ("real_diff_minus", @{thm real_diff_minus}); |
130 if Rule_Set.contains r1 Test_simplify then () |
130 if Rule_Set.contains r1 Test_simplify then () |
131 else error "rewtools.sml Rule_Set.contains Thm"; |
131 else error "rewtools.sml Rule_Set.contains Thm"; |
132 |
132 |
133 val r1 = Eval (\<^const_name>\<open>plus\<close>, eval_binop "#add_"); |
133 val r1 = Eval (\<^const_name>\<open>plus\<close>, eval_binop "#add_"); |
134 if Rule_Set.contains r1 Test_simplify then () |
134 if Rule_Set.contains r1 Test_simplify then () |