changeset 8902 | a705822f4e2a |
parent 7982 | d534b897ce39 |
child 9477 | 9506127f6fbb |
--- a/src/HOL/Isar_examples/BasicLogic.thy Sun May 21 14:44:01 2000 +0200 +++ b/src/HOL/Isar_examples/BasicLogic.thy Sun May 21 14:49:28 2000 +0200 @@ -228,12 +228,12 @@ lemma "A & B --> B & A"; proof -; - {{; + {; assume ab: "A & B"; from ab; have a: A; ..; from ab; have b: B; ..; from b a; have "B & A"; ..; - }}; + }; thus ?thesis; .. -- {* rule \name{impI} *}; qed;