--- /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
--- 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"