equal
deleted
inserted
replaced
2079 (FIXME: check whether @{ML Pattern.match_rew} and @{ML Pattern.rewrite_term} |
2079 (FIXME: check whether @{ML Pattern.match_rew} and @{ML Pattern.rewrite_term} |
2080 are of any use/efficient) |
2080 are of any use/efficient) |
2081 *} |
2081 *} |
2082 |
2082 |
2083 |
2083 |
|
2084 section {* Declarations (TBD) *} |
|
2085 |
2084 section {* Structured Proofs (TBD) *} |
2086 section {* Structured Proofs (TBD) *} |
2085 |
2087 |
2086 text {* TBD *} |
2088 text {* TBD *} |
2087 |
2089 |
2088 lemma True |
2090 lemma True |
2103 note conjI [OF this] |
2105 note conjI [OF this] |
2104 note r [OF this] |
2106 note r [OF this] |
2105 } |
2107 } |
2106 oops |
2108 oops |
2107 |
2109 |
2108 ML {* fun prop ctxt s = |
|
2109 Thm.cterm_of (ProofContext.theory_of ctxt) (Syntax.read_prop ctxt s) *} |
|
2110 |
|
2111 ML {* |
2110 ML {* |
2112 val ctxt0 = @{context}; |
2111 val ctxt0 = @{context}; |
2113 val ctxt = ctxt0; |
2112 val ctxt = ctxt0; |
2114 val (_, ctxt) = Variable.add_fixes ["A", "B", "C"] ctxt; |
2113 val (_, ctxt) = Variable.add_fixes ["A", "B", "C"] ctxt; |
2115 val ([r], ctxt) = Assumption.add_assumes [prop ctxt "A & B \<Longrightarrow> C"] ctxt; |
2114 val ([r], ctxt) = Assumption.add_assumes [@{cprop "A & B \<Longrightarrow> C"}] ctxt |
2116 val (this, ctxt) = Assumption.add_assumes [prop ctxt "A", prop ctxt "B"] ctxt; |
2115 val (this, ctxt) = Assumption.add_assumes [@{cprop "A"}, @{cprop "B"}] ctxt; |
2117 val this = [@{thm conjI} OF this]; |
2116 val this = [@{thm conjI} OF this]; |
2118 val this = r OF this; |
2117 val this = r OF this; |
2119 val this = Assumption.export false ctxt ctxt0 this |
2118 val this = Assumption.export false ctxt ctxt0 this |
2120 val this = Variable.export ctxt ctxt0 [this] |
2119 val this = Variable.export ctxt ctxt0 [this] |
2121 *} |
2120 *} |