src/HOL/Isar_examples/BasicLogic.thy

     Author:     Markus Wenzel, TU Muenchen
 
 Basic propositional and quantifier reasoning.
 *)
 
+header {* Basic reasoning *};
+
 theory BasicLogic = Main:;
-
 
 subsection {* Some trivialities *};
 
 text {* Just a few toy examples to get an idea of how Isabelle/Isar
   proof documents may look like. *};

 lemma I: "A --> A";
 proof;
   assume A;
   show A; .;
 qed;
-
 
 lemma K: "A --> B --> A";
 proof;
   assume A;
   show "B --> A";

 qed;
 
 lemma K''': "A --> B --> A";
   by intro;
 
-
 lemma S: "(A --> B --> C) --> (A --> B) --> A --> C";
 proof;
   assume "A --> B --> C";
   show "(A --> B) --> A --> C";
   proof;

         show B; by (rule mp);
       qed;
     qed;
   qed;
 qed;
-
 
 text {* Variations of backward vs.\ forward reasoning \dots *};
 
 lemma "A & B --> B & A";
 proof;

     from ab; show A; ..;
     from ab; show B; ..;
   qed;
 qed;
 
-
 end;