755 | Const(@{const_name Groups.uminus},_)$s => isnum s |
755 | Const(@{const_name Groups.uminus},_)$s => isnum s |
756 | Const(@{const_name Groups.plus},_)$l$r => isnum l andalso isnum r |
756 | Const(@{const_name Groups.plus},_)$l$r => isnum l andalso isnum r |
757 | Const(@{const_name Groups.times},_)$l$r => isnum l andalso isnum r |
757 | Const(@{const_name Groups.times},_)$l$r => isnum l andalso isnum r |
758 | Const(@{const_name Groups.minus},_)$l$r => isnum l andalso isnum r |
758 | Const(@{const_name Groups.minus},_)$l$r => isnum l andalso isnum r |
759 | Const(@{const_name Power.power},_)$l$r => isnum l andalso isnum r |
759 | Const(@{const_name Power.power},_)$l$r => isnum l andalso isnum r |
760 | Const(@{const_name Divides.mod},_)$l$r => isnum l andalso isnum r |
760 | Const(@{const_name Rings.modulo},_)$l$r => isnum l andalso isnum r |
761 | Const(@{const_name Rings.divide},_)$l$r => isnum l andalso isnum r |
761 | Const(@{const_name Rings.divide},_)$l$r => isnum l andalso isnum r |
762 | _ => is_number t orelse can HOLogic.dest_nat t |
762 | _ => is_number t orelse can HOLogic.dest_nat t |
763 |
763 |
764 fun ty cts t = |
764 fun ty cts t = |
765 if not (member (op =) [HOLogic.intT, HOLogic.natT, HOLogic.boolT] (Thm.typ_of_cterm t)) |
765 if not (member (op =) [HOLogic.intT, HOLogic.natT, HOLogic.boolT] (Thm.typ_of_cterm t)) |