equal
deleted
inserted
replaced
832 Below we change \isacommand{foobar} so that it takes a proposition as |
832 Below we change \isacommand{foobar} so that it takes a proposition as |
833 argument and then starts a proof in order to prove it. Therefore in Line 13, |
833 argument and then starts a proof in order to prove it. Therefore in Line 13, |
834 we set the kind indicator to @{ML thy_goal in OuterKeyword}. |
834 we set the kind indicator to @{ML thy_goal in OuterKeyword}. |
835 *} |
835 *} |
836 |
836 |
837 ML%linenumbers{*let |
837 ML%linenosgray{*let |
838 fun set_up_thm str ctxt = |
838 fun set_up_thm str ctxt = |
839 let |
839 let |
840 val prop = Syntax.read_prop ctxt str |
840 val prop = Syntax.read_prop ctxt str |
841 in |
841 in |
842 Proof.theorem_i NONE (K I) [[(prop,[])]] ctxt |
842 Proof.theorem_i NONE (K I) [[(prop,[])]] ctxt |