# HG changeset patch
# User wenzelm
# Date 1451154466 -3600
# Node ID 6512e84cc9f5d3d21bb5fc889a72904949bed120
# Parent  02610a8064678251e5afc979d478dc6e2ee28290
clarified sessions;

diff -r 02610a806467 -r 6512e84cc9f5 src/FOL/ROOT
--- a/src/FOL/ROOT	Sat Dec 26 16:10:00 2015 +0100
+++ b/src/FOL/ROOT	Sat Dec 26 19:27:46 2015 +0100
@@ -25,7 +25,6 @@
     Examples for First-Order Logic.
   *}
   theories
-    First_Order_Logic
     Natural_Numbers
     Intro
     Nat
diff -r 02610a806467 -r 6512e84cc9f5 src/FOL/ex/First_Order_Logic.thy
--- a/src/FOL/ex/First_Order_Logic.thy	Sat Dec 26 16:10:00 2015 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,161 +0,0 @@
-(*  Title:      FOL/ex/First_Order_Logic.thy
-    Author:     Makarius
-*)
-
-section \<open>A simple formulation of First-Order Logic\<close>
-
-text \<open>
-  The subsequent theory development illustrates single-sorted intuitionistic
-  first-order logic with equality, formulated within the Pure framework. So
-  this is strictly speaking an example of Isabelle/Pure, not Isabelle/FOL.
-\<close>
-
-theory First_Order_Logic
-imports Pure
-begin
-
-subsection \<open>Abstract syntax\<close>
-
-typedecl i
-typedecl o
-
-judgment Trueprop :: "o \<Rightarrow> prop"  ("_" 5)
-
-
-subsection \<open>Propositional logic\<close>
-
-axiomatization false :: o  ("\<bottom>")
-  where falseE [elim]: "\<bottom> \<Longrightarrow> A"
-
-
-axiomatization imp :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<longrightarrow>" 25)
-  where impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"
-    and mp [dest]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B"
-
-
-axiomatization conj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<and>" 35)
-  where conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
-    and conjD1: "A \<and> B \<Longrightarrow> A"
-    and conjD2: "A \<and> B \<Longrightarrow> B"
-
-theorem conjE [elim]:
-  assumes "A \<and> B"
-  obtains A and B
-proof
-  from \<open>A \<and> B\<close> show A
-    by (rule conjD1)
-  from \<open>A \<and> B\<close> show B
-    by (rule conjD2)
-qed
-
-
-axiomatization disj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<or>" 30)
-  where disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C"
-    and disjI1 [intro]: "A \<Longrightarrow> A \<or> B"
-    and disjI2 [intro]: "B \<Longrightarrow> A \<or> B"
-
-
-definition true :: o  ("\<top>")
-  where "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
-
-theorem trueI [intro]: \<top>
-  unfolding true_def ..
-
-
-definition not :: "o \<Rightarrow> o"  ("\<not> _" [40] 40)
-  where "\<not> A \<equiv> A \<longrightarrow> \<bottom>"
-
-theorem notI [intro]: "(A \<Longrightarrow> \<bottom>) \<Longrightarrow> \<not> A"
-  unfolding not_def ..
-
-theorem notE [elim]: "\<not> A \<Longrightarrow> A \<Longrightarrow> B"
-  unfolding not_def
-proof -
-  assume "A \<longrightarrow> \<bottom>" and A
-  then have \<bottom> ..
-  then show B ..
-qed
-
-
-definition iff :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<longleftrightarrow>" 25)
-  where "A \<longleftrightarrow> B \<equiv> (A \<longrightarrow> B) \<and> (B \<longrightarrow> A)"
-
-theorem iffI [intro]:
-  assumes "A \<Longrightarrow> B"
-    and "B \<Longrightarrow> A"
-  shows "A \<longleftrightarrow> B"
-  unfolding iff_def
-proof
-  from \<open>A \<Longrightarrow> B\<close> show "A \<longrightarrow> B" ..
-  from \<open>B \<Longrightarrow> A\<close> show "B \<longrightarrow> A" ..
-qed
-
-theorem iff1 [elim]:
-  assumes "A \<longleftrightarrow> B" and A
-  shows B
-proof -
-  from \<open>A \<longleftrightarrow> B\<close> have "(A \<longrightarrow> B) \<and> (B \<longrightarrow> A)"
-    unfolding iff_def .
-  then have "A \<longrightarrow> B" ..
-  from this and \<open>A\<close> show B ..
-qed
-
-theorem iff2 [elim]:
-  assumes "A \<longleftrightarrow> B" and B
-  shows A
-proof -
-  from \<open>A \<longleftrightarrow> B\<close> have "(A \<longrightarrow> B) \<and> (B \<longrightarrow> A)"
-    unfolding iff_def .
-  then have "B \<longrightarrow> A" ..
-  from this and \<open>B\<close> show A ..
-qed
-
-
-subsection \<open>Equality\<close>
-
-axiomatization equal :: "i \<Rightarrow> i \<Rightarrow> o"  (infixl "=" 50)
-  where refl [intro]: "x = x"
-    and subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y"
-
-theorem trans [trans]: "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"
-  by (rule subst)
-
-theorem sym [sym]: "x = y \<Longrightarrow> y = x"
-proof -
-  assume "x = y"
-  from this and refl show "y = x"
-    by (rule subst)
-qed
-
-
-subsection \<open>Quantifiers\<close>
-
-axiomatization All :: "(i \<Rightarrow> o) \<Rightarrow> o"  (binder "\<forall>" 10)
-  where allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x"
-    and allD [dest]: "\<forall>x. P x \<Longrightarrow> P a"
-
-axiomatization Ex :: "(i \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>" 10)
-  where exI [intro]: "P a \<Longrightarrow> \<exists>x. P x"
-    and exE [elim]: "\<exists>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> C) \<Longrightarrow> C"
-
-
-lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"
-proof
-  assume "\<exists>x. P (f x)"
-  then obtain x where "P (f x)" ..
-  then show "\<exists>y. P y" ..
-qed
-
-lemma "(\<exists>x. \<forall>y. R x y) \<longrightarrow> (\<forall>y. \<exists>x. R x y)"
-proof
-  assume "\<exists>x. \<forall>y. R x y"
-  then obtain x where "\<forall>y. R x y" ..
-  show "\<forall>y. \<exists>x. R x y"
-  proof
-    fix y
-    from \<open>\<forall>y. R x y\<close> have "R x y" ..
-    then show "\<exists>x. R x y" ..
-  qed
-qed
-
-end
diff -r 02610a806467 -r 6512e84cc9f5 src/HOL/Induct/Nested_Datatype.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Nested_Datatype.thy	Sat Dec 26 19:27:46 2015 +0100
@@ -0,0 +1,61 @@
+section \<open>Nested datatypes\<close>
+
+theory Nested_Datatype
+imports Main
+begin
+
+subsection \<open>Terms and substitution\<close>
+
+datatype ('a, 'b) "term" =
+  Var 'a
+| App 'b "('a, 'b) term list"
+
+primrec subst_term :: "('a \<Rightarrow> ('a, 'b) term) \<Rightarrow> ('a, 'b) term \<Rightarrow> ('a, 'b) term"
+  and subst_term_list :: "('a \<Rightarrow> ('a, 'b) term) \<Rightarrow> ('a, 'b) term list \<Rightarrow> ('a, 'b) term list"
+where
+  "subst_term f (Var a) = f a"
+| "subst_term f (App b ts) = App b (subst_term_list f ts)"
+| "subst_term_list f [] = []"
+| "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
+
+lemmas subst_simps = subst_term.simps subst_term_list.simps
+
+text \<open>\<^medskip> A simple lemma about composition of substitutions.\<close>
+
+lemma
+  "subst_term (subst_term f1 \<circ> f2) t =
+    subst_term f1 (subst_term f2 t)"
+  and
+  "subst_term_list (subst_term f1 \<circ> f2) ts =
+    subst_term_list f1 (subst_term_list f2 ts)"
+  by (induct t and ts rule: subst_term.induct subst_term_list.induct) simp_all
+
+lemma "subst_term (subst_term f1 \<circ> f2) t = subst_term f1 (subst_term f2 t)"
+proof -
+  let "?P t" = ?thesis
+  let ?Q = "\<lambda>ts. subst_term_list (subst_term f1 \<circ> f2) ts =
+    subst_term_list f1 (subst_term_list f2 ts)"
+  show ?thesis
+  proof (induct t rule: subst_term.induct)
+    show "?P (Var a)" for a by simp
+    show "?P (App b ts)" if "?Q ts" for b ts
+      using that by (simp only: subst_simps)
+    show "?Q []" by simp
+    show "?Q (t # ts)" if "?P t" "?Q ts" for t ts
+      using that by (simp only: subst_simps)
+  qed
+qed
+
+
+subsection \<open>Alternative induction\<close>
+
+lemma "subst_term (subst_term f1 \<circ> f2) t = subst_term f1 (subst_term f2 t)"
+proof (induct t rule: term.induct)
+  case (Var a)
+  show ?case by (simp add: o_def)
+next
+  case (App b ts)
+  then show ?case by (induct ts) simp_all
+qed
+
+end
diff -r 02610a806467 -r 6512e84cc9f5 src/HOL/Isar_Examples/First_Order_Logic.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Isar_Examples/First_Order_Logic.thy	Sat Dec 26 19:27:46 2015 +0100
@@ -0,0 +1,160 @@
+(*  Title:      HOL/Isar_Examples/First_Order_Logic.thy
+    Author:     Makarius
+*)
+
+section \<open>A simple formulation of First-Order Logic\<close>
+
+text \<open>
+  The subsequent theory development illustrates single-sorted intuitionistic
+  first-order logic with equality, formulated within the Pure framework.
+\<close>
+
+theory First_Order_Logic
+imports Pure
+begin
+
+subsection \<open>Abstract syntax\<close>
+
+typedecl i
+typedecl o
+
+judgment Trueprop :: "o \<Rightarrow> prop"  ("_" 5)
+
+
+subsection \<open>Propositional logic\<close>
+
+axiomatization false :: o  ("\<bottom>")
+  where falseE [elim]: "\<bottom> \<Longrightarrow> A"
+
+
+axiomatization imp :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<longrightarrow>" 25)
+  where impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"
+    and mp [dest]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B"
+
+
+axiomatization conj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<and>" 35)
+  where conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
+    and conjD1: "A \<and> B \<Longrightarrow> A"
+    and conjD2: "A \<and> B \<Longrightarrow> B"
+
+theorem conjE [elim]:
+  assumes "A \<and> B"
+  obtains A and B
+proof
+  from \<open>A \<and> B\<close> show A
+    by (rule conjD1)
+  from \<open>A \<and> B\<close> show B
+    by (rule conjD2)
+qed
+
+
+axiomatization disj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<or>" 30)
+  where disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C"
+    and disjI1 [intro]: "A \<Longrightarrow> A \<or> B"
+    and disjI2 [intro]: "B \<Longrightarrow> A \<or> B"
+
+
+definition true :: o  ("\<top>")
+  where "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
+
+theorem trueI [intro]: \<top>
+  unfolding true_def ..
+
+
+definition not :: "o \<Rightarrow> o"  ("\<not> _" [40] 40)
+  where "\<not> A \<equiv> A \<longrightarrow> \<bottom>"
+
+theorem notI [intro]: "(A \<Longrightarrow> \<bottom>) \<Longrightarrow> \<not> A"
+  unfolding not_def ..
+
+theorem notE [elim]: "\<not> A \<Longrightarrow> A \<Longrightarrow> B"
+  unfolding not_def
+proof -
+  assume "A \<longrightarrow> \<bottom>" and A
+  then have \<bottom> ..
+  then show B ..
+qed
+
+
+definition iff :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<longleftrightarrow>" 25)
+  where "A \<longleftrightarrow> B \<equiv> (A \<longrightarrow> B) \<and> (B \<longrightarrow> A)"
+
+theorem iffI [intro]:
+  assumes "A \<Longrightarrow> B"
+    and "B \<Longrightarrow> A"
+  shows "A \<longleftrightarrow> B"
+  unfolding iff_def
+proof
+  from \<open>A \<Longrightarrow> B\<close> show "A \<longrightarrow> B" ..
+  from \<open>B \<Longrightarrow> A\<close> show "B \<longrightarrow> A" ..
+qed
+
+theorem iff1 [elim]:
+  assumes "A \<longleftrightarrow> B" and A
+  shows B
+proof -
+  from \<open>A \<longleftrightarrow> B\<close> have "(A \<longrightarrow> B) \<and> (B \<longrightarrow> A)"
+    unfolding iff_def .
+  then have "A \<longrightarrow> B" ..
+  from this and \<open>A\<close> show B ..
+qed
+
+theorem iff2 [elim]:
+  assumes "A \<longleftrightarrow> B" and B
+  shows A
+proof -
+  from \<open>A \<longleftrightarrow> B\<close> have "(A \<longrightarrow> B) \<and> (B \<longrightarrow> A)"
+    unfolding iff_def .
+  then have "B \<longrightarrow> A" ..
+  from this and \<open>B\<close> show A ..
+qed
+
+
+subsection \<open>Equality\<close>
+
+axiomatization equal :: "i \<Rightarrow> i \<Rightarrow> o"  (infixl "=" 50)
+  where refl [intro]: "x = x"
+    and subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y"
+
+theorem trans [trans]: "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"
+  by (rule subst)
+
+theorem sym [sym]: "x = y \<Longrightarrow> y = x"
+proof -
+  assume "x = y"
+  from this and refl show "y = x"
+    by (rule subst)
+qed
+
+
+subsection \<open>Quantifiers\<close>
+
+axiomatization All :: "(i \<Rightarrow> o) \<Rightarrow> o"  (binder "\<forall>" 10)
+  where allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x"
+    and allD [dest]: "\<forall>x. P x \<Longrightarrow> P a"
+
+axiomatization Ex :: "(i \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>" 10)
+  where exI [intro]: "P a \<Longrightarrow> \<exists>x. P x"
+    and exE [elim]: "\<exists>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> C) \<Longrightarrow> C"
+
+
+lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"
+proof
+  assume "\<exists>x. P (f x)"
+  then obtain x where "P (f x)" ..
+  then show "\<exists>y. P y" ..
+qed
+
+lemma "(\<exists>x. \<forall>y. R x y) \<longrightarrow> (\<forall>y. \<exists>x. R x y)"
+proof
+  assume "\<exists>x. \<forall>y. R x y"
+  then obtain x where "\<forall>y. R x y" ..
+  show "\<forall>y. \<exists>x. R x y"
+  proof
+    fix y
+    from \<open>\<forall>y. R x y\<close> have "R x y" ..
+    then show "\<exists>x. R x y" ..
+  qed
+qed
+
+end
diff -r 02610a806467 -r 6512e84cc9f5 src/HOL/Isar_Examples/Higher_Order_Logic.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Isar_Examples/Higher_Order_Logic.thy	Sat Dec 26 19:27:46 2015 +0100
@@ -0,0 +1,327 @@
+(*  Title:      HOL/Isar_Examples/Higher_Order_Logic.thy
+    Author:     Makarius
+*)
+
+section \<open>Foundations of HOL\<close>
+
+theory Higher_Order_Logic
+imports Pure
+begin
+
+text \<open>
+  The following theory development demonstrates Higher-Order Logic itself,
+  represented directly within the Pure framework of Isabelle. The ``HOL''
+  logic given here is essentially that of Gordon @{cite "Gordon:1985:HOL"},
+  although we prefer to present basic concepts in a slightly more conventional
+  manner oriented towards plain Natural Deduction.
+\<close>
+
+
+subsection \<open>Pure Logic\<close>
+
+class type
+default_sort type
+
+typedecl o
+instance o :: type ..
+instance "fun" :: (type, type) type ..
+
+
+subsubsection \<open>Basic logical connectives\<close>
+
+judgment Trueprop :: "o \<Rightarrow> prop"  ("_" 5)
+
+axiomatization imp :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<longrightarrow>" 25)
+  where impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"
+    and impE [dest, trans]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B"
+
+axiomatization All :: "('a \<Rightarrow> o) \<Rightarrow> o"  (binder "\<forall>" 10)
+  where allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x"
+    and allE [dest]: "\<forall>x. P x \<Longrightarrow> P a"
+
+
+subsubsection \<open>Extensional equality\<close>
+
+axiomatization equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"  (infixl "=" 50)
+  where refl [intro]: "x = x"
+    and subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y"
+
+axiomatization
+  where ext [intro]: "(\<And>x. f x = g x) \<Longrightarrow> f = g"
+    and iff [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A = B"
+
+theorem sym [sym]:
+  assumes "x = y"
+  shows "y = x"
+  using assms by (rule subst) (rule refl)
+
+lemma [trans]: "x = y \<Longrightarrow> P y \<Longrightarrow> P x"
+  by (rule subst) (rule sym)
+
+lemma [trans]: "P x \<Longrightarrow> x = y \<Longrightarrow> P y"
+  by (rule subst)
+
+theorem trans [trans]: "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"
+  by (rule subst)
+
+theorem iff1 [elim]: "A = B \<Longrightarrow> A \<Longrightarrow> B"
+  by (rule subst)
+
+theorem iff2 [elim]: "A = B \<Longrightarrow> B \<Longrightarrow> A"
+  by (rule subst) (rule sym)
+
+
+subsubsection \<open>Derived connectives\<close>
+
+definition false :: o  ("\<bottom>") where "\<bottom> \<equiv> \<forall>A. A"
+
+theorem falseE [elim]:
+  assumes "\<bottom>"
+  shows A
+proof -
+  from \<open>\<bottom>\<close> have "\<forall>A. A" unfolding false_def .
+  then show A ..
+qed
+
+
+definition true :: o  ("\<top>") where "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
+
+theorem trueI [intro]: \<top>
+  unfolding true_def ..
+
+
+definition not :: "o \<Rightarrow> o"  ("\<not> _" [40] 40)
+  where "not \<equiv> \<lambda>A. A \<longrightarrow> \<bottom>"
+
+abbreviation not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"  (infixl "\<noteq>" 50)
+  where "x \<noteq> y \<equiv> \<not> (x = y)"
+
+theorem notI [intro]:
+  assumes "A \<Longrightarrow> \<bottom>"
+  shows "\<not> A"
+  using assms unfolding not_def ..
+
+theorem notE [elim]:
+  assumes "\<not> A" and A
+  shows B
+proof -
+  from \<open>\<not> A\<close> have "A \<longrightarrow> \<bottom>" unfolding not_def .
+  from this and \<open>A\<close> have "\<bottom>" ..
+  then show B ..
+qed
+
+lemma notE': "A \<Longrightarrow> \<not> A \<Longrightarrow> B"
+  by (rule notE)
+
+lemmas contradiction = notE notE'  \<comment> \<open>proof by contradiction in any order\<close>
+
+
+definition conj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<and>" 35)
+  where "conj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
+
+theorem conjI [intro]:
+  assumes A and B
+  shows "A \<and> B"
+  unfolding conj_def
+proof
+  fix C
+  show "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
+  proof
+    assume "A \<longrightarrow> B \<longrightarrow> C"
+    also note \<open>A\<close>
+    also note \<open>B\<close>
+    finally show C .
+  qed
+qed
+
+theorem conjE [elim]:
+  assumes "A \<and> B"
+  obtains A and B
+proof
+  from \<open>A \<and> B\<close> have *: "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C" for C
+    unfolding conj_def ..
+  show A
+  proof -
+    note * [of A]
+    also have "A \<longrightarrow> B \<longrightarrow> A"
+    proof
+      assume A
+      then show "B \<longrightarrow> A" ..
+    qed
+    finally show ?thesis .
+  qed
+  show B
+  proof -
+    note * [of B]
+    also have "A \<longrightarrow> B \<longrightarrow> B"
+    proof
+      show "B \<longrightarrow> B" ..
+    qed
+    finally show ?thesis .
+  qed
+qed
+
+
+definition disj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<or>" 30)
+  where "disj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
+
+theorem disjI1 [intro]:
+  assumes A
+  shows "A \<or> B"
+  unfolding disj_def
+proof
+  fix C
+  show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
+  proof
+    assume "A \<longrightarrow> C"
+    from this and \<open>A\<close> have C ..
+    then show "(B \<longrightarrow> C) \<longrightarrow> C" ..
+  qed
+qed
+
+theorem disjI2 [intro]:
+  assumes B
+  shows "A \<or> B"
+  unfolding disj_def
+proof
+  fix C
+  show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
+  proof
+    show "(B \<longrightarrow> C) \<longrightarrow> C"
+    proof
+      assume "B \<longrightarrow> C"
+      from this and \<open>B\<close> show C ..
+    qed
+  qed
+qed
+
+theorem disjE [elim]:
+  assumes "A \<or> B"
+  obtains (a) A | (b) B
+proof -
+  from \<open>A \<or> B\<close> have "(A \<longrightarrow> thesis) \<longrightarrow> (B \<longrightarrow> thesis) \<longrightarrow> thesis"
+    unfolding disj_def ..
+  also have "A \<longrightarrow> thesis"
+  proof
+    assume A
+    then show thesis by (rule a)
+  qed
+  also have "B \<longrightarrow> thesis"
+  proof
+    assume B
+    then show thesis by (rule b)
+  qed
+  finally show thesis .
+qed
+
+
+definition Ex :: "('a \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>" 10)
+  where "\<exists>x. P x \<equiv> \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
+
+theorem exI [intro]: "P a \<Longrightarrow> \<exists>x. P x"
+  unfolding Ex_def
+proof
+  fix C
+  assume "P a"
+  show "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
+  proof
+    assume "\<forall>x. P x \<longrightarrow> C"
+    then have "P a \<longrightarrow> C" ..
+    from this and \<open>P a\<close> show C ..
+  qed
+qed
+
+theorem exE [elim]:
+  assumes "\<exists>x. P x"
+  obtains (that) x where "P x"
+proof -
+  from \<open>\<exists>x. P x\<close> have "(\<forall>x. P x \<longrightarrow> thesis) \<longrightarrow> thesis"
+    unfolding Ex_def ..
+  also have "\<forall>x. P x \<longrightarrow> thesis"
+  proof
+    fix x
+    show "P x \<longrightarrow> thesis"
+    proof
+      assume "P x"
+      then show thesis by (rule that)
+    qed
+  qed
+  finally show thesis .
+qed
+
+
+subsection \<open>Classical logic\<close>
+
+text \<open>
+  The subsequent rules of classical reasoning are all equivalent.
+\<close>
+
+locale classical =
+  assumes classical: "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"
+
+theorem (in classical) Peirce's_Law: "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
+proof
+  assume a: "(A \<longrightarrow> B) \<longrightarrow> A"
+  show A
+  proof (rule classical)
+    assume "\<not> A"
+    have "A \<longrightarrow> B"
+    proof
+      assume A
+      with \<open>\<not> A\<close> show B by (rule contradiction)
+    qed
+    with a show A ..
+  qed
+qed
+
+theorem (in classical) double_negation:
+  assumes "\<not> \<not> A"
+  shows A
+proof (rule classical)
+  assume "\<not> A"
+  with \<open>\<not> \<not> A\<close> show ?thesis by (rule contradiction)
+qed
+
+theorem (in classical) tertium_non_datur: "A \<or> \<not> A"
+proof (rule double_negation)
+  show "\<not> \<not> (A \<or> \<not> A)"
+  proof
+    assume "\<not> (A \<or> \<not> A)"
+    have "\<not> A"
+    proof
+      assume A then have "A \<or> \<not> A" ..
+      with \<open>\<not> (A \<or> \<not> A)\<close> show \<bottom> by (rule contradiction)
+    qed
+    then have "A \<or> \<not> A" ..
+    with \<open>\<not> (A \<or> \<not> A)\<close> show \<bottom> by (rule contradiction)
+  qed
+qed
+
+theorem (in classical) classical_cases:
+  obtains A | "\<not> A"
+  using tertium_non_datur
+proof
+  assume A
+  then show thesis ..
+next
+  assume "\<not> A"
+  then show thesis ..
+qed
+
+lemma
+  assumes classical_cases: "\<And>A C. (A \<Longrightarrow> C) \<Longrightarrow> (\<not> A \<Longrightarrow> C) \<Longrightarrow> C"
+  shows "PROP classical"
+proof
+  fix A
+  assume *: "\<not> A \<Longrightarrow> A"
+  show A
+  proof (rule classical_cases)
+    assume A
+    then show A .
+  next
+    assume "\<not> A"
+    then show A by (rule *)
+  qed
+qed
+
+end
diff -r 02610a806467 -r 6512e84cc9f5 src/HOL/Isar_Examples/Nested_Datatype.thy
--- a/src/HOL/Isar_Examples/Nested_Datatype.thy	Sat Dec 26 16:10:00 2015 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,61 +0,0 @@
-section \<open>Nested datatypes\<close>
-
-theory Nested_Datatype
-imports Main
-begin
-
-subsection \<open>Terms and substitution\<close>
-
-datatype ('a, 'b) "term" =
-  Var 'a
-| App 'b "('a, 'b) term list"
-
-primrec subst_term :: "('a \<Rightarrow> ('a, 'b) term) \<Rightarrow> ('a, 'b) term \<Rightarrow> ('a, 'b) term"
-  and subst_term_list :: "('a \<Rightarrow> ('a, 'b) term) \<Rightarrow> ('a, 'b) term list \<Rightarrow> ('a, 'b) term list"
-where
-  "subst_term f (Var a) = f a"
-| "subst_term f (App b ts) = App b (subst_term_list f ts)"
-| "subst_term_list f [] = []"
-| "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
-
-lemmas subst_simps = subst_term.simps subst_term_list.simps
-
-text \<open>\<^medskip> A simple lemma about composition of substitutions.\<close>
-
-lemma
-  "subst_term (subst_term f1 \<circ> f2) t =
-    subst_term f1 (subst_term f2 t)"
-  and
-  "subst_term_list (subst_term f1 \<circ> f2) ts =
-    subst_term_list f1 (subst_term_list f2 ts)"
-  by (induct t and ts rule: subst_term.induct subst_term_list.induct) simp_all
-
-lemma "subst_term (subst_term f1 \<circ> f2) t = subst_term f1 (subst_term f2 t)"
-proof -
-  let "?P t" = ?thesis
-  let ?Q = "\<lambda>ts. subst_term_list (subst_term f1 \<circ> f2) ts =
-    subst_term_list f1 (subst_term_list f2 ts)"
-  show ?thesis
-  proof (induct t rule: subst_term.induct)
-    show "?P (Var a)" for a by simp
-    show "?P (App b ts)" if "?Q ts" for b ts
-      using that by (simp only: subst_simps)
-    show "?Q []" by simp
-    show "?Q (t # ts)" if "?P t" "?Q ts" for t ts
-      using that by (simp only: subst_simps)
-  qed
-qed
-
-
-subsection \<open>Alternative induction\<close>
-
-lemma "subst_term (subst_term f1 \<circ> f2) t = subst_term f1 (subst_term f2 t)"
-proof (induct t rule: term.induct)
-  case (Var a)
-  show ?case by (simp add: o_def)
-next
-  case (App b ts)
-  then show ?case by (induct ts) simp_all
-qed
-
-end
diff -r 02610a806467 -r 6512e84cc9f5 src/HOL/Isar_Examples/document/root.bib
--- a/src/HOL/Isar_Examples/document/root.bib	Sat Dec 26 16:10:00 2015 +0100
+++ b/src/HOL/Isar_Examples/document/root.bib	Sat Dec 26 19:27:46 2015 +0100
@@ -44,6 +44,14 @@
   publisher	= CUP,
   year		= 1990}
 
+@TechReport{Gordon:1985:HOL,
+  author =       {M. J. C. Gordon},
+  title =        {{HOL}: A machine oriented formulation of higher order logic},
+  institution =  {University of Cambridge Computer Laboratory},
+  year =         1985,
+  number =       68
+}
+
 @manual{isabelle-HOL,
   author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
   title		= {{Isabelle}'s Logics: {HOL}},
diff -r 02610a806467 -r 6512e84cc9f5 src/HOL/Isar_Examples/document/root.tex
--- a/src/HOL/Isar_Examples/document/root.tex	Sat Dec 26 16:10:00 2015 +0100
+++ b/src/HOL/Isar_Examples/document/root.tex	Sat Dec 26 19:27:46 2015 +0100
@@ -15,7 +15,7 @@
 
 \begin{document}
 
-\title{Miscellaneous Isabelle/Isar examples for Higher-Order Logic}
+\title{Miscellaneous Isabelle/Isar examples}
 \author{Makarius Wenzel \\[2ex]
   With contributions by Gertrud Bauer and Tobias Nipkow}
 \maketitle
diff -r 02610a806467 -r 6512e84cc9f5 src/HOL/ROOT
--- a/src/HOL/ROOT	Sat Dec 26 16:10:00 2015 +0100
+++ b/src/HOL/ROOT	Sat Dec 26 19:27:46 2015 +0100
@@ -99,6 +99,7 @@
   theories [quick_and_dirty]
     Common_Patterns
   theories
+    Nested_Datatype
     QuoDataType
     QuoNestedDataType
     Term
@@ -548,7 +549,6 @@
     Adhoc_Overloading_Examples
     Iff_Oracle
     Coercion_Examples
-    Higher_Order_Logic
     Abstract_NAT
     Guess
     Fundefs
@@ -622,11 +622,13 @@
 
 session "HOL-Isar_Examples" in Isar_Examples = HOL +
   description {*
-    Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
+    Miscellaneous Isabelle/Isar examples.
   *}
   theories [document = false]
     "~~/src/HOL/Library/Lattice_Syntax"
     "../Number_Theory/Primes"
+  theories [quick_and_dirty]
+    Structured_Statements
   theories
     Basic_Logic
     Cantor
@@ -639,12 +641,11 @@
     Hoare_Ex
     Knaster_Tarski
     Mutilated_Checkerboard
-    Nested_Datatype
     Peirce
     Puzzle
     Summation
-  theories [quick_and_dirty]
-    Structured_Statements
+    First_Order_Logic
+    Higher_Order_Logic
   document_files
     "root.bib"
     "root.tex"
diff -r 02610a806467 -r 6512e84cc9f5 src/HOL/ex/Higher_Order_Logic.thy
--- a/src/HOL/ex/Higher_Order_Logic.thy	Sat Dec 26 16:10:00 2015 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,327 +0,0 @@
-(*  Title:      HOL/ex/Higher_Order_Logic.thy
-    Author:     Makarius
-*)
-
-section \<open>Foundations of HOL\<close>
-
-theory Higher_Order_Logic
-imports Pure
-begin
-
-text \<open>
-  The following theory development demonstrates Higher-Order Logic itself,
-  represented directly within the Pure framework of Isabelle. The ``HOL''
-  logic given here is essentially that of Gordon @{cite "Gordon:1985:HOL"},
-  although we prefer to present basic concepts in a slightly more conventional
-  manner oriented towards plain Natural Deduction.
-\<close>
-
-
-subsection \<open>Pure Logic\<close>
-
-class type
-default_sort type
-
-typedecl o
-instance o :: type ..
-instance "fun" :: (type, type) type ..
-
-
-subsubsection \<open>Basic logical connectives\<close>
-
-judgment Trueprop :: "o \<Rightarrow> prop"  ("_" 5)
-
-axiomatization imp :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<longrightarrow>" 25)
-  where impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"
-    and impE [dest, trans]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B"
-
-axiomatization All :: "('a \<Rightarrow> o) \<Rightarrow> o"  (binder "\<forall>" 10)
-  where allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x"
-    and allE [dest]: "\<forall>x. P x \<Longrightarrow> P a"
-
-
-subsubsection \<open>Extensional equality\<close>
-
-axiomatization equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"  (infixl "=" 50)
-  where refl [intro]: "x = x"
-    and subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y"
-
-axiomatization
-  where ext [intro]: "(\<And>x. f x = g x) \<Longrightarrow> f = g"
-    and iff [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A = B"
-
-theorem sym [sym]:
-  assumes "x = y"
-  shows "y = x"
-  using assms by (rule subst) (rule refl)
-
-lemma [trans]: "x = y \<Longrightarrow> P y \<Longrightarrow> P x"
-  by (rule subst) (rule sym)
-
-lemma [trans]: "P x \<Longrightarrow> x = y \<Longrightarrow> P y"
-  by (rule subst)
-
-theorem trans [trans]: "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"
-  by (rule subst)
-
-theorem iff1 [elim]: "A = B \<Longrightarrow> A \<Longrightarrow> B"
-  by (rule subst)
-
-theorem iff2 [elim]: "A = B \<Longrightarrow> B \<Longrightarrow> A"
-  by (rule subst) (rule sym)
-
-
-subsubsection \<open>Derived connectives\<close>
-
-definition false :: o  ("\<bottom>") where "\<bottom> \<equiv> \<forall>A. A"
-
-theorem falseE [elim]:
-  assumes "\<bottom>"
-  shows A
-proof -
-  from \<open>\<bottom>\<close> have "\<forall>A. A" unfolding false_def .
-  then show A ..
-qed
-
-
-definition true :: o  ("\<top>") where "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
-
-theorem trueI [intro]: \<top>
-  unfolding true_def ..
-
-
-definition not :: "o \<Rightarrow> o"  ("\<not> _" [40] 40)
-  where "not \<equiv> \<lambda>A. A \<longrightarrow> \<bottom>"
-
-abbreviation not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"  (infixl "\<noteq>" 50)
-  where "x \<noteq> y \<equiv> \<not> (x = y)"
-
-theorem notI [intro]:
-  assumes "A \<Longrightarrow> \<bottom>"
-  shows "\<not> A"
-  using assms unfolding not_def ..
-
-theorem notE [elim]:
-  assumes "\<not> A" and A
-  shows B
-proof -
-  from \<open>\<not> A\<close> have "A \<longrightarrow> \<bottom>" unfolding not_def .
-  from this and \<open>A\<close> have "\<bottom>" ..
-  then show B ..
-qed
-
-lemma notE': "A \<Longrightarrow> \<not> A \<Longrightarrow> B"
-  by (rule notE)
-
-lemmas contradiction = notE notE'  \<comment> \<open>proof by contradiction in any order\<close>
-
-
-definition conj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<and>" 35)
-  where "conj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
-
-theorem conjI [intro]:
-  assumes A and B
-  shows "A \<and> B"
-  unfolding conj_def
-proof
-  fix C
-  show "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
-  proof
-    assume "A \<longrightarrow> B \<longrightarrow> C"
-    also note \<open>A\<close>
-    also note \<open>B\<close>
-    finally show C .
-  qed
-qed
-
-theorem conjE [elim]:
-  assumes "A \<and> B"
-  obtains A and B
-proof
-  from \<open>A \<and> B\<close> have *: "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C" for C
-    unfolding conj_def ..
-  show A
-  proof -
-    note * [of A]
-    also have "A \<longrightarrow> B \<longrightarrow> A"
-    proof
-      assume A
-      then show "B \<longrightarrow> A" ..
-    qed
-    finally show ?thesis .
-  qed
-  show B
-  proof -
-    note * [of B]
-    also have "A \<longrightarrow> B \<longrightarrow> B"
-    proof
-      show "B \<longrightarrow> B" ..
-    qed
-    finally show ?thesis .
-  qed
-qed
-
-
-definition disj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<or>" 30)
-  where "disj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
-
-theorem disjI1 [intro]:
-  assumes A
-  shows "A \<or> B"
-  unfolding disj_def
-proof
-  fix C
-  show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
-  proof
-    assume "A \<longrightarrow> C"
-    from this and \<open>A\<close> have C ..
-    then show "(B \<longrightarrow> C) \<longrightarrow> C" ..
-  qed
-qed
-
-theorem disjI2 [intro]:
-  assumes B
-  shows "A \<or> B"
-  unfolding disj_def
-proof
-  fix C
-  show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
-  proof
-    show "(B \<longrightarrow> C) \<longrightarrow> C"
-    proof
-      assume "B \<longrightarrow> C"
-      from this and \<open>B\<close> show C ..
-    qed
-  qed
-qed
-
-theorem disjE [elim]:
-  assumes "A \<or> B"
-  obtains (a) A | (b) B
-proof -
-  from \<open>A \<or> B\<close> have "(A \<longrightarrow> thesis) \<longrightarrow> (B \<longrightarrow> thesis) \<longrightarrow> thesis"
-    unfolding disj_def ..
-  also have "A \<longrightarrow> thesis"
-  proof
-    assume A
-    then show thesis by (rule a)
-  qed
-  also have "B \<longrightarrow> thesis"
-  proof
-    assume B
-    then show thesis by (rule b)
-  qed
-  finally show thesis .
-qed
-
-
-definition Ex :: "('a \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>" 10)
-  where "\<exists>x. P x \<equiv> \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
-
-theorem exI [intro]: "P a \<Longrightarrow> \<exists>x. P x"
-  unfolding Ex_def
-proof
-  fix C
-  assume "P a"
-  show "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
-  proof
-    assume "\<forall>x. P x \<longrightarrow> C"
-    then have "P a \<longrightarrow> C" ..
-    from this and \<open>P a\<close> show C ..
-  qed
-qed
-
-theorem exE [elim]:
-  assumes "\<exists>x. P x"
-  obtains (that) x where "P x"
-proof -
-  from \<open>\<exists>x. P x\<close> have "(\<forall>x. P x \<longrightarrow> thesis) \<longrightarrow> thesis"
-    unfolding Ex_def ..
-  also have "\<forall>x. P x \<longrightarrow> thesis"
-  proof
-    fix x
-    show "P x \<longrightarrow> thesis"
-    proof
-      assume "P x"
-      then show thesis by (rule that)
-    qed
-  qed
-  finally show thesis .
-qed
-
-
-subsection \<open>Classical logic\<close>
-
-text \<open>
-  The subsequent rules of classical reasoning are all equivalent.
-\<close>
-
-locale classical =
-  assumes classical: "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"
-
-theorem (in classical) Peirce's_Law: "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
-proof
-  assume a: "(A \<longrightarrow> B) \<longrightarrow> A"
-  show A
-  proof (rule classical)
-    assume "\<not> A"
-    have "A \<longrightarrow> B"
-    proof
-      assume A
-      with \<open>\<not> A\<close> show B by (rule contradiction)
-    qed
-    with a show A ..
-  qed
-qed
-
-theorem (in classical) double_negation:
-  assumes "\<not> \<not> A"
-  shows A
-proof (rule classical)
-  assume "\<not> A"
-  with \<open>\<not> \<not> A\<close> show ?thesis by (rule contradiction)
-qed
-
-theorem (in classical) tertium_non_datur: "A \<or> \<not> A"
-proof (rule double_negation)
-  show "\<not> \<not> (A \<or> \<not> A)"
-  proof
-    assume "\<not> (A \<or> \<not> A)"
-    have "\<not> A"
-    proof
-      assume A then have "A \<or> \<not> A" ..
-      with \<open>\<not> (A \<or> \<not> A)\<close> show \<bottom> by (rule contradiction)
-    qed
-    then have "A \<or> \<not> A" ..
-    with \<open>\<not> (A \<or> \<not> A)\<close> show \<bottom> by (rule contradiction)
-  qed
-qed
-
-theorem (in classical) classical_cases:
-  obtains A | "\<not> A"
-  using tertium_non_datur
-proof
-  assume A
-  then show thesis ..
-next
-  assume "\<not> A"
-  then show thesis ..
-qed
-
-lemma
-  assumes classical_cases: "\<And>A C. (A \<Longrightarrow> C) \<Longrightarrow> (\<not> A \<Longrightarrow> C) \<Longrightarrow> C"
-  shows "PROP classical"
-proof
-  fix A
-  assume *: "\<not> A \<Longrightarrow> A"
-  show A
-  proof (rule classical_cases)
-    assume A
-    then show A .
-  next
-    assume "\<not> A"
-    then show A by (rule *)
-  qed
-qed
-
-end
diff -r 02610a806467 -r 6512e84cc9f5 src/HOL/ex/document/root.bib
--- a/src/HOL/ex/document/root.bib	Sat Dec 26 16:10:00 2015 +0100
+++ b/src/HOL/ex/document/root.bib	Sat Dec 26 19:27:46 2015 +0100
@@ -1,11 +1,3 @@
-@TechReport{Gordon:1985:HOL,
-  author =       {M. J. C. Gordon},
-  title =        {{HOL}: A machine oriented formulation of higher order logic},
-  institution =  {University of Cambridge Computer Laboratory},
-  year =         1985,
-  number =       68
-}
-
 @inproceedings{HuttonW04,author={Graham Hutton and Joel Wright},
 title={Compiling Exceptions Correctly},
 booktitle={Proc.\ Conf.\ Mathematics of Program Construction},