equal
deleted
inserted
replaced
172 FIXME: All below is your construction code; mostly commented out as it |
172 FIXME: All below is your construction code; mostly commented out as it |
173 does not work. |
173 does not work. |
174 *) |
174 *) |
175 |
175 |
176 ML {* |
176 ML {* |
177 mk_REGULARIZE_goal @{context} |
177 mk_regularize_trm @{context} |
178 @{term "\<forall>i j k. my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"} |
178 @{term "\<forall>i j k. my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"} |
179 @{term "\<forall>i j k. PLUS (PLUS i j) k = PLUS i (PLUS j k)"} |
179 @{term "\<forall>i j k. PLUS (PLUS i j) k = PLUS i (PLUS j k)"} |
180 |> Syntax.string_of_term @{context} |
180 |> Syntax.string_of_term @{context} |
181 |> writeln |
181 |> writeln |
182 *} |
182 *} |