equal
deleted
inserted
replaced
70 val with_facts_i: (thm * Proof.context attribute list) list * Comment.text |
70 val with_facts_i: (thm * Proof.context attribute list) list * Comment.text |
71 -> ProofHistory.T -> ProofHistory.T |
71 -> ProofHistory.T -> ProofHistory.T |
72 val chain: Comment.text -> ProofHistory.T -> ProofHistory.T |
72 val chain: Comment.text -> ProofHistory.T -> ProofHistory.T |
73 val export_chain: Comment.text -> ProofHistory.T -> ProofHistory.T |
73 val export_chain: Comment.text -> ProofHistory.T -> ProofHistory.T |
74 val fix: ((string list * string option) * Comment.text) list -> ProofHistory.T -> ProofHistory.T |
74 val fix: ((string list * string option) * Comment.text) list -> ProofHistory.T -> ProofHistory.T |
75 val fix_i: ((string list * typ) * Comment.text) list -> ProofHistory.T -> ProofHistory.T |
75 val fix_i: ((string list * typ option) * Comment.text) list -> ProofHistory.T -> ProofHistory.T |
76 val match_bind: ((string list * string) * Comment.text) list -> ProofHistory.T -> ProofHistory.T |
76 val match_bind: ((string list * string) * Comment.text) list -> ProofHistory.T -> ProofHistory.T |
77 val match_bind_i: ((term list * term) * Comment.text) list -> ProofHistory.T -> ProofHistory.T |
77 val match_bind_i: ((term list * term) * Comment.text) list -> ProofHistory.T -> ProofHistory.T |
78 val theorem: (bstring * Args.src list * (string * (string list * string list))) |
78 val theorem: (bstring * Args.src list * (string * (string list * string list))) |
79 * Comment.text -> bool -> theory -> ProofHistory.T |
79 * Comment.text -> bool -> theory -> ProofHistory.T |
80 val theorem_i: (bstring * theory attribute list * (term * (term list * term list))) |
80 val theorem_i: (bstring * theory attribute list * (term * (term list * term list))) |
91 * Comment.text) list -> ProofHistory.T -> ProofHistory.T |
91 * Comment.text) list -> ProofHistory.T -> ProofHistory.T |
92 val presume_i: ((string * Proof.context attribute list * (term * (term list * term list)) list) |
92 val presume_i: ((string * Proof.context attribute list * (term * (term list * term list)) list) |
93 * Comment.text) list -> ProofHistory.T -> ProofHistory.T |
93 * Comment.text) list -> ProofHistory.T -> ProofHistory.T |
94 val local_def: (string * Args.src list * ((string * string option) * (string * string list))) |
94 val local_def: (string * Args.src list * ((string * string option) * (string * string list))) |
95 * Comment.text -> ProofHistory.T -> ProofHistory.T |
95 * Comment.text -> ProofHistory.T -> ProofHistory.T |
96 val local_def_i: (string * Args.src list * ((string * typ) * (term * term list))) |
96 val local_def_i: (string * Args.src list * ((string * typ option) * (term * term list))) |
97 * Comment.text -> ProofHistory.T -> ProofHistory.T |
97 * Comment.text -> ProofHistory.T -> ProofHistory.T |
98 val show: (string * Args.src list * (string * (string list * string list))) |
98 val show: (string * Args.src list * (string * (string list * string list))) |
99 * Comment.text -> ProofHistory.T -> ProofHistory.T |
99 * Comment.text -> ProofHistory.T -> ProofHistory.T |
100 val show_i: (string * Proof.context attribute list * (term * (term list * term list))) |
100 val show_i: (string * Proof.context attribute list * (term * (term list * term list))) |
101 * Comment.text -> ProofHistory.T -> ProofHistory.T |
101 * Comment.text -> ProofHistory.T -> ProofHistory.T |