--- a/src/HOL/Isar_examples/BasicLogic.thy Tue Oct 05 21:20:28 1999 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy Wed Oct 06 00:31:40 1999 +0200
@@ -5,9 +5,10 @@
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
@@ -19,7 +20,6 @@
show A; .;
qed;
-
lemma K: "A --> B --> A";
proof;
assume A;
@@ -44,7 +44,6 @@
lemma K''': "A --> B --> A";
by intro;
-
lemma S: "(A --> B --> C) --> (A --> B) --> A --> C";
proof;
assume "A --> B --> C";
@@ -63,7 +62,6 @@
qed;
qed;
-
text {* Variations of backward vs.\ forward reasoning \dots *};
lemma "A & B --> B & A";
@@ -178,5 +176,4 @@
qed;
qed;
-
end;