669 |
669 |
670 (*reorientation simplification procedure: reorients (polymorphic) |
670 (*reorientation simplification procedure: reorients (polymorphic) |
671 0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*) |
671 0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*) |
672 fun reorient_proc sg _ (_ $ t $ u) = |
672 fun reorient_proc sg _ (_ $ t $ u) = |
673 case u of |
673 case u of |
674 Const(@{const_name HOL.zero}, _) => NONE |
674 Const(@{const_name Algebras.zero}, _) => NONE |
675 | Const(@{const_name HOL.one}, _) => NONE |
675 | Const(@{const_name Algebras.one}, _) => NONE |
676 | Const(@{const_name Int.number_of}, _) $ _ => NONE |
676 | Const(@{const_name Int.number_of}, _) $ _ => NONE |
677 | _ => SOME (case t of |
677 | _ => SOME (case t of |
678 Const(@{const_name HOL.zero}, _) => meta_zero_approx_reorient |
678 Const(@{const_name Algebras.zero}, _) => meta_zero_approx_reorient |
679 | Const(@{const_name HOL.one}, _) => meta_one_approx_reorient |
679 | Const(@{const_name Algebras.one}, _) => meta_one_approx_reorient |
680 | Const(@{const_name Int.number_of}, _) $ _ => |
680 | Const(@{const_name Int.number_of}, _) $ _ => |
681 meta_number_of_approx_reorient); |
681 meta_number_of_approx_reorient); |
682 |
682 |
683 in |
683 in |
684 val approx_reorient_simproc = |
684 val approx_reorient_simproc = |