tuned;
authorwenzelm
Sat Sep 25 13:18:38 1999 +0200 (1999-09-25 ago)
changeset 760455566b9ec7d7
parent 7603 b2b5599b934f
child 7605 8bbfcb54054e
tuned;
src/HOL/Isar_examples/BasicLogic.thy
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/HOL/Isar_examples/BasicLogic.thy	Sat Sep 25 13:18:20 1999 +0200
     1.2 +++ b/src/HOL/Isar_examples/BasicLogic.thy	Sat Sep 25 13:18:38 1999 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  theory BasicLogic = Main:;
     1.5  
     1.6  
     1.7 -text {* Just a few tiny examples to get an idea of how Isabelle/Isar
     1.8 +text {* Just a few toy examples to get an idea of how Isabelle/Isar
     1.9    proof documents may look like. *};
    1.10  
    1.11  lemma I: "A --> A";
    1.12 @@ -62,7 +62,7 @@
    1.13  qed;
    1.14  
    1.15  
    1.16 -text {* Variations of backward vs.\ forward reasonong \dots *};
    1.17 +text {* Variations of backward vs.\ forward reasoning \dots *};
    1.18  
    1.19  lemma "A & B --> B & A";
    1.20  proof;
    1.21 @@ -86,6 +86,16 @@
    1.22  
    1.23  lemma "A & B --> B & A";
    1.24  proof;
    1.25 +  assume "A & B";
    1.26 +  show "B & A";
    1.27 +  proof;
    1.28 +    from prems; show B; ..;
    1.29 +    from prems; show A; ..;
    1.30 +  qed;
    1.31 +qed;
    1.32 +
    1.33 +lemma "A & B --> B & A";
    1.34 +proof;
    1.35    assume ab: "A & B";
    1.36    from ab; have a: A; ..;
    1.37    from ab; have b: B; ..;
     2.1 --- a/src/Pure/Isar/outer_syntax.ML	Sat Sep 25 13:18:20 1999 +0200
     2.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sat Sep 25 13:18:38 1999 +0200
     2.3 @@ -345,7 +345,8 @@
     2.4  fun isar term no_pos =
     2.5    Source.tty
     2.6    |> Symbol.source true
     2.7 -  |> OuterLex.source true get_lexicons (if no_pos then Position.none else Position.line_name 1 "stdin")
     2.8 +  |> OuterLex.source true get_lexicons
     2.9 +    (if no_pos then Position.none else Position.line_name 1 "stdin")
    2.10    |> source term true get_parser;
    2.11  
    2.12