summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Tue, 19 Dec 2000 15:24:55 +0100 | |

changeset 10707 | 9285b4d87d7d |

parent 10706 | f02834001fca |

child 10708 | 1a6348a11489 |

re-orienting equations with #nnn on the lhs

--- a/src/HOL/Numeral.ML Tue Dec 19 15:20:23 2000 +0100 +++ b/src/HOL/Numeral.ML Tue Dec 19 15:24:55 2000 +0100 @@ -8,3 +8,11 @@ by(Simp_tac 1); qed "Let_number_of"; Addsimps [Let_number_of]; + +(*The condition "True" is a hack to prevent looping. + Conditional rewrite rules are tried after unconditional ones, so a rule + like eq_nat_number_of will be tried first to eliminate #mm=#nn. *) +Goal "True ==> (number_of w = x) = (x = number_of w)"; +by Auto_tac; +qed "number_of_reorient"; +Addsimps [number_of_reorient];