equal
deleted
inserted
replaced
212 val def_of_const : theory -> const_table * const_table -> styp -> term option |
212 val def_of_const : theory -> const_table * const_table -> styp -> term option |
213 val fixpoint_kind_of_rhs : term -> fixpoint_kind |
213 val fixpoint_kind_of_rhs : term -> fixpoint_kind |
214 val fixpoint_kind_of_const : |
214 val fixpoint_kind_of_const : |
215 theory -> const_table * const_table -> string * typ -> fixpoint_kind |
215 theory -> const_table * const_table -> string * typ -> fixpoint_kind |
216 val is_real_inductive_pred : hol_context -> styp -> bool |
216 val is_real_inductive_pred : hol_context -> styp -> bool |
|
217 val is_constr_pattern : Proof.context -> term -> bool |
217 val is_constr_pattern_lhs : Proof.context -> term -> bool |
218 val is_constr_pattern_lhs : Proof.context -> term -> bool |
218 val is_constr_pattern_formula : Proof.context -> term -> bool |
219 val is_constr_pattern_formula : Proof.context -> term -> bool |
219 val nondef_props_for_const : |
220 val nondef_props_for_const : |
220 theory -> bool -> const_table -> styp -> term list |
221 theory -> bool -> const_table -> styp -> term list |
221 val is_choice_spec_fun : hol_context -> styp -> bool |
222 val is_choice_spec_fun : hol_context -> styp -> bool |