summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Integ/NatSimprocs.ML

changeset 11464 | ddea204de5bc |

parent 11296 | 38a69e5d79fa |

child 11468 | 02cd5d5bc497 |

1.1 --- a/src/HOL/Integ/NatSimprocs.ML Mon Aug 06 13:12:06 2001 +0200 1.2 +++ b/src/HOL/Integ/NatSimprocs.ML Mon Aug 06 13:43:24 2001 +0200 1.3 @@ -14,13 +14,15 @@ 1.4 1.5 (*Now just instantiating n to (number_of v) does the right simplification, 1.6 but with some redundant inequality tests.*) 1.7 - 1.8 +(* 1.9 Goal "neg (number_of (bin_pred v)) = (number_of v = (0::nat))"; 1.10 by (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < 1)" 1); 1.11 by (Asm_simp_tac 1); 1.12 by (stac less_number_of_Suc 1); 1.13 by (Simp_tac 1); 1.14 qed "neg_number_of_bin_pred_iff_0"; 1.15 +*) 1.16 +val neg_number_of_bin_pred_iff_0 = thm "neg_number_of_bin_pred_iff_0"; 1.17 1.18 Goal "neg (number_of (bin_minus v)) ==> \ 1.19 \ Suc m - (number_of v) = m - (number_of (bin_pred v))";