# HG changeset patch # User wenzelm # Date 938258318 -7200 # Node ID 55566b9ec7d742c157447908135bac35e8ee2892 # Parent b2b5599b934fe58668d3bc3e4d46cfd6e3921fd8 tuned; diff -r b2b5599b934f -r 55566b9ec7d7 src/HOL/Isar_examples/BasicLogic.thy --- a/src/HOL/Isar_examples/BasicLogic.thy Sat Sep 25 13:18:20 1999 +0200 +++ b/src/HOL/Isar_examples/BasicLogic.thy Sat Sep 25 13:18:38 1999 +0200 @@ -8,7 +8,7 @@ theory BasicLogic = Main:; -text {* Just a few tiny examples to get an idea of how Isabelle/Isar +text {* Just a few toy examples to get an idea of how Isabelle/Isar proof documents may look like. *}; lemma I: "A --> A"; @@ -62,7 +62,7 @@ qed; -text {* Variations of backward vs.\ forward reasonong \dots *}; +text {* Variations of backward vs.\ forward reasoning \dots *}; lemma "A & B --> B & A"; proof; @@ -86,6 +86,16 @@ lemma "A & B --> B & A"; proof; + assume "A & B"; + show "B & A"; + proof; + from prems; show B; ..; + from prems; show A; ..; + qed; +qed; + +lemma "A & B --> B & A"; +proof; assume ab: "A & B"; from ab; have a: A; ..; from ab; have b: B; ..; diff -r b2b5599b934f -r 55566b9ec7d7 src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Sat Sep 25 13:18:20 1999 +0200 +++ b/src/Pure/Isar/outer_syntax.ML Sat Sep 25 13:18:38 1999 +0200 @@ -345,7 +345,8 @@ fun isar term no_pos = Source.tty |> Symbol.source true - |> OuterLex.source true get_lexicons (if no_pos then Position.none else Position.line_name 1 "stdin") + |> OuterLex.source true get_lexicons + (if no_pos then Position.none else Position.line_name 1 "stdin") |> source term true get_parser;