equal
deleted
inserted
replaced
152 val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int |
152 val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int |
153 val bounded_exact_card_of_type : |
153 val bounded_exact_card_of_type : |
154 hol_context -> typ list -> int -> int -> (typ * int) list -> typ -> int |
154 hol_context -> typ list -> int -> int -> (typ * int) list -> typ -> int |
155 val is_finite_type : hol_context -> typ -> bool |
155 val is_finite_type : hol_context -> typ -> bool |
156 val special_bounds : term list -> (indexname * typ) list |
156 val special_bounds : term list -> (indexname * typ) list |
|
157 val abs_var : indexname * typ -> term -> term |
157 val is_funky_typedef : theory -> typ -> bool |
158 val is_funky_typedef : theory -> typ -> bool |
158 val all_axioms_of : |
159 val all_axioms_of : |
159 theory -> (term * term) list -> term list * term list * term list |
160 theory -> (term * term) list -> term list * term list * term list |
160 val arity_of_built_in_const : |
161 val arity_of_built_in_const : |
161 theory -> (typ option * bool) list -> bool -> styp -> int option |
162 theory -> (typ option * bool) list -> bool -> styp -> int option |
629 | NONE => try (snd o HOLogic.dest_mem o HOLogic.dest_Trueprop) |
630 | NONE => try (snd o HOLogic.dest_mem o HOLogic.dest_Trueprop) |
630 prop_of_Rep |
631 prop_of_Rep |
631 in |
632 in |
632 case t_opt of |
633 case t_opt of |
633 SOME (Const (@{const_name top}, _)) => true |
634 SOME (Const (@{const_name top}, _)) => true |
|
635 (* "Multiset.multiset" *) |
634 | SOME (Const (@{const_name Collect}, _) |
636 | SOME (Const (@{const_name Collect}, _) |
635 $ Abs (_, _, Const (@{const_name finite}, _) $ _)) => true |
637 $ Abs (_, _, Const (@{const_name finite}, _) $ _)) => true |
|
638 (* "FinFun.finfun" *) |
|
639 | SOME (Const (@{const_name Collect}, _) $ Abs (_, _, |
|
640 Const (@{const_name Ex}, _) $ Abs (_, _, |
|
641 Const (@{const_name finite}, _) $ _))) => true |
636 | _ => false |
642 | _ => false |
637 end |
643 end |
638 | NONE => false) |
644 | NONE => false) |
639 | is_univ_typedef _ _ = false |
645 | is_univ_typedef _ _ = false |
640 (* theory -> (typ option * bool) list -> typ -> bool *) |
646 (* theory -> (typ option * bool) list -> typ -> bool *) |