equal
deleted
inserted
replaced
2105 note conjI [OF this] |
2105 note conjI [OF this] |
2106 note r [OF this] |
2106 note r [OF this] |
2107 } |
2107 } |
2108 oops |
2108 oops |
2109 |
2109 |
2110 ML {* fun prop ctxt s = |
|
2111 Thm.cterm_of (ProofContext.theory_of ctxt) (Syntax.read_prop ctxt s) *} |
|
2112 |
|
2113 ML {* |
2110 ML {* |
2114 val ctxt0 = @{context}; |
2111 val ctxt0 = @{context}; |
2115 val ctxt = ctxt0; |
2112 val ctxt = ctxt0; |
2116 val (_, ctxt) = Variable.add_fixes ["A", "B", "C"] ctxt; |
2113 val (_, ctxt) = Variable.add_fixes ["A", "B", "C"] ctxt; |
2117 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 |
2118 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; |
2119 val this = [@{thm conjI} OF this]; |
2116 val this = [@{thm conjI} OF this]; |
2120 val this = r OF this; |
2117 val this = r OF this; |
2121 val this = Assumption.export false ctxt ctxt0 this |
2118 val this = Assumption.export false ctxt ctxt0 this |
2122 val this = Variable.export ctxt ctxt0 [this] |
2119 val this = Variable.export ctxt ctxt0 [this] |
2123 *} |
2120 *} |