| changeset 1655 | 5be64540f275 |
| parent 1626 | 12560b3ebf2c |
| child 1660 | 8cb42cd97579 |
--- a/src/HOL/Arith.ML Tue Apr 09 12:12:27 1996 +0200 +++ b/src/HOL/Arith.ML Thu Apr 11 08:30:25 1996 +0200 @@ -27,7 +27,7 @@ (** Difference **) -val diff_0 = diff_def RS def_nat_rec_0; +bind_thm("diff_0", diff_def RS def_nat_rec_0); qed_goalw "diff_0_eq_0" Arith.thy [diff_def, pred_def] "0 - n = 0"