src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 41994 c567c860caf6
parent 41898 55d981e1232a
child 42361 23f352990944
equal deleted inserted replaced
41993:bd6296de1432 41994:c567c860caf6
   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