Mike Gordon wrote:
> HOL nicely simplifies natural number expressions, e.g.:
>
> - SIMP_CONV arith_ss [] ``?(i:num) (j:num). i <= j``;
> > val it = [oracles: DISK_THM] [axioms: ] [] |- (?i j. i <= j) = T : thm
>
> however, I can't figure out how to get this for integer expressions, e.g.:
>
>
HOL nicely simplifies natural number expressions, e.g.:
- SIMP_CONV arith_ss [] ``?(i:num) (j:num). i <= j``;
> val it = [oracles: DISK_THM] [axioms: ] [] |- (?i j. i <= j) = T : thm
however, I can't figure out how to get this for integer expressions, e.g.:
- SIMP_CONV int_ss [] ``?(i:int) (
