# 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;