src/HOL/Isar_examples/BasicLogic.thy

 Basic propositional and quantifier 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";

   from ab; have b: B; ..;
   from b a; show "B & A"; ..;
 qed;
 
 
-section {* Examples from 'Introduction to Isabelle' *};
+subsection {* A few examples from ``Introduction to Isabelle'' *};
 
-text {* 'Propositional proof' *};
+subsubsection {* Propositional proof *};
 
 lemma "P | P --> P";
 proof;
   assume "P | P";
   then; show P;

   assume "P | P";
   then; show P; ..;
 qed;
 
 
-text {* 'Quantifier proof' *};
+subsubsection {* Quantifier proof *};
 
 lemma "(EX x. P(f(x))) --> (EX x. P(x))";
 proof;
   assume "EX x. P(f(x))";
   then; show "EX x. P(x)";

 
 lemma "(EX x. P(f(x))) --> (EX x. P(x))";
   by blast;
 
 
-subsection {* 'Deriving rules in Isabelle' *};
+subsubsection {* Deriving rules in Isabelle *};
 
 text {* We derive the conjunction elimination rule from the
  projections.  The proof below follows the basic reasoning of the
  script given in the Isabelle Intro Manual closely.  Although, the
  actual underlying operations on rules and proof states are quite