equal
deleted
inserted
replaced
4 Context assumptions, parameterized by export rules. |
4 Context assumptions, parameterized by export rules. |
5 *) |
5 *) |
6 |
6 |
7 signature ASSUMPTION = |
7 signature ASSUMPTION = |
8 sig |
8 sig |
9 type export |
9 type export = bool -> cterm list -> (thm -> thm) * (term -> term) |
10 val assume_export: export |
10 val assume_export: export |
11 val presume_export: export |
11 val presume_export: export |
12 val assume: cterm -> thm |
12 val assume: cterm -> thm |
13 val all_assms_of: Proof.context -> cterm list |
13 val all_assms_of: Proof.context -> cterm list |
14 val all_prems_of: Proof.context -> thm list |
14 val all_prems_of: Proof.context -> thm list |