equal
deleted
inserted
replaced
2103 val theorem_in_locale = |
2103 val theorem_in_locale = |
2104 gen_theorem_in_locale intern Attrib.intern_src intern_attrib_elem_expr read_context_statement; |
2104 gen_theorem_in_locale intern Attrib.intern_src intern_attrib_elem_expr read_context_statement; |
2105 val theorem_in_locale_i = |
2105 val theorem_in_locale_i = |
2106 gen_theorem_in_locale (K I) (K I) (K I) cert_context_statement; |
2106 gen_theorem_in_locale (K I) (K I) (K I) cert_context_statement; |
2107 |
2107 |
2108 fun smart_theorem kind NONE a [] concl = (* FIXME tune *) |
2108 fun smart_theorem kind NONE a [] concl = |
2109 Proof.theorem kind (K (K I)) NONE a concl o ProofContext.init |
2109 Proof.theorem kind (K (K I)) NONE a concl o ProofContext.init |
2110 | smart_theorem kind NONE a elems concl = |
2110 | smart_theorem kind NONE a elems concl = |
2111 theorem kind (K (K I)) a elems concl |
2111 theorem kind (K (K I)) a elems concl |
2112 | smart_theorem kind (SOME loc) a elems concl = |
2112 | smart_theorem kind (SOME loc) a elems concl = |
2113 theorem_in_locale kind (K (K I)) loc a elems concl; |
2113 theorem_in_locale kind (K (K I)) loc a elems concl; |