# HG changeset patch
# User wenzelm
# Date 1434194317 -7200
# Node ID b54b913dfa6ac86b853e34576261d443e48a17dc
# Parent  229bad93377e0f27eee3bbf4a5378fd7e12c1214
more examples;

diff -r 229bad93377e -r b54b913dfa6a src/HOL/Isar_Examples/Structured_Statements.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Isar_Examples/Structured_Statements.thy	Sat Jun 13 13:18:37 2015 +0200
@@ -0,0 +1,44 @@
+(*  Title:      HOL/Isar_Examples/Structured_Statements.thy
+    Author:     Makarius
+*)
+
+section \<open>Structured statements within Isar proofs\<close>
+
+theory Structured_Statements
+imports Main
+begin
+
+notepad
+begin
+
+  fix A B :: bool
+
+  have iff_comm: "(A \<and> B) \<longleftrightarrow> (B \<and> A)"
+  proof
+    show "B \<and> A" if "A \<and> B"
+    proof
+      show B using that ..
+      show A using that ..
+    qed
+    show "A \<and> B" if "B \<and> A"
+    proof
+      show A using that ..
+      show B using that ..
+    qed
+  qed
+
+  text \<open>Alternative proof, avoiding redundant copy of symmetric argument.\<close>
+  have iff_comm: "(A \<and> B) \<longleftrightarrow> (B \<and> A)"
+  proof
+    show "B \<and> A" if "A \<and> B" for A B
+    proof
+      show B using that ..
+      show A using that ..
+    qed
+    then show "A \<and> B" if "B \<and> A"
+      by this (rule that)
+  qed
+
+end
+
+end
\ No newline at end of file
diff -r 229bad93377e -r b54b913dfa6a src/HOL/ROOT
--- a/src/HOL/ROOT	Sat Jun 13 13:09:05 2015 +0200
+++ b/src/HOL/ROOT	Sat Jun 13 13:18:37 2015 +0200
@@ -623,6 +623,7 @@
     Peirce
     Puzzle
     Summation
+    Structured_Statements
   document_files
     "root.bib"
     "root.tex"