changeset 21539 | c5cf9243ad62 |
parent 20342 | 4392003fcbfa |
child 23071 | bf058e6405f8 |
--- a/src/ZF/Integ/int_arith.ML Sun Nov 26 23:09:25 2006 +0100 +++ b/src/ZF/Integ/int_arith.ML Sun Nov 26 23:43:53 2006 +0100 @@ -20,7 +20,7 @@ AddIffs [inst "y" "integ_of(?w)" zminus_zle, inst "x" "integ_of(?w)" zle_zminus]; -Addsimps [inst "s" "integ_of(?w)" Let_def]; +Addsimps [inst "s" "integ_of(?w)" (thm "Let_def")]; (*** Simprocs for numeric literals ***)