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) (j:int). i <= j``; ! Uncaught exception: ! UNCHANGED Anyone know if there is a simpset for integers that works on examples like this? Mike ------------------------------------------------------------------------- This SF.Net email is sponsored by the Moblin Your Move Developer's challenge Build the coolest Linux based applications with Moblin SDK & win great prizes Grand prize is a trip for two to an Open Source event anywhere in the world http://moblin-contest.org/redirect.php?banner_id=100&url=/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
