type 'term inductive =
{ inductive_id : id ;
+ inductive_name : string;
inductive_kind : bool;
inductive_type : 'term;
inductive_constructors : 'term declaration list
and 'term in_proof_context_element =
[ 'term decl_context_element
- | ('term,'term proof) def_context_element
+ | ('term,'term proof) def_context_element
| ('term,'term proof) joint_context_element
]
and lemma =
{ lemma_id: id;
lemma_name : string;
- lemma_uri: string
+ lemma_uri: string
}
;;