Lines Matching defs:proof
16 type proof = string;
91 (Attrib.binding * string) list)) * proof
93 (Attrib.binding * string) list) * proof
98 |Subclass of opt_target * string * proof
101 |Instance of (instance_type option) * proof
105 (Element.context list * Element.statement)) * proof
108 (Element.context list * Element.statement)) * proof
111 (Element.context list * Element.statement)) * proof
115 proof
118 (Element.context list * Element.statement)) * proof
122 proof
134 * (Attrib.binding * string) list)) * proof
135 |Termination of string option * proof
137 string) * (binding * binding) option) * proof
242 command_with_args "proof"
255 val proof = Parse.!!! ((proof_prefix -- Scan.first
256 [command_with_args "proof" -- proof_qed 1 >> op@,
424 -- proof
428 -- proof >> Interpretation),
433 Parse.class -- proof >> Parse.triple1 >> Subclass),
439 -- proof >> Instance),
440 ("theorem", parse_theorem -- proof >> Theorem), (* line 525 *)
441 ("lemma", parse_theorem -- proof >> Lemma), (* line 526 *)
442 ("corollary", parse_theorem -- proof >> Corollary),(* line 527 *)
443 ("schematic_theorem", parse_theorem -- proof (* line 528 *)
445 ("schematic_lemma", parse_theorem -- proof (* line 529 *)
447 ("schematic_corollary", parse_theorem -- proof (* line 530 *)
469 -- proof
472 ("termination",Scan.option Parse.term -- proof
480 proof >> Typedef),
1043 fn Typedef (((((vars,tp),mx),tm),morphisms),proof) =>
1058 (mx'@[xml "Proof" [] [XML.Text proof]]@
1074 fn Instance (head,proof) =>
1092 ([xml "Proof" [] [XML.Text proof]]@elems), s1) end,
1093 fn Subclass (target,cls,proof) =>
1098 [xml "Proof" [] [XML.Text proof]],
1192 fn Lemma ((((target,(name,args)), strs),(ctxt,stmt)),proof) =>
1199 (ctxt'::[xml "Proof" [] [XML.Text proof]]