src/HOL/BNF_FP_Base.thy
changeset 55642 63beb38e9258
parent 55575 a5e33e18fb5c
child 55700 cf6a029b28d8
     1.1 --- a/src/HOL/BNF_FP_Base.thy	Fri Feb 21 00:09:55 2014 +0100
     1.2 +++ b/src/HOL/BNF_FP_Base.thy	Fri Feb 21 00:09:56 2014 +0100
     1.3 @@ -20,7 +20,7 @@
     1.4  by blast
     1.5  
     1.6  lemma case_unit_Unity: "(case u of () \<Rightarrow> f) = f"
     1.7 -by (cases u) (hypsubst, rule unit.cases)
     1.8 +by (cases u) (hypsubst, rule unit.case)
     1.9  
    1.10  lemma case_prod_Pair_iden: "(case p of (x, y) \<Rightarrow> (x, y)) = p"
    1.11  by simp