src/HOL/ex/Simps_Case_Conv_Examples.thy

--- a/src/HOL/ex/Simps_Case_Conv_Examples.thy	Thu Jul 09 15:45:00 2015 +0200
+++ b/src/HOL/ex/Simps_Case_Conv_Examples.thy	Thu Jul 09 15:52:11 2015 +0200
@@ -75,6 +75,11 @@
   "test (Some x) y = x"
   by (fact test_simps1)+
 
+text {* Single-constructor patterns*}
+case_of_simps fst_conv_simps: fst_conv
+lemma "fst x = (case x of (a,b) \<Rightarrow> a)"
+  by (fact fst_conv_simps)
+
 text {* Partial split of case *}
 simps_of_case nosplit_simps2: nosplit_def (splits: list.split)
 lemma