src/HOL/Imperative_HOL/Heap_Monad.thy
changeset 35423 6ef9525a5727
parent 35113 1a0c129bb2e0
child 36057 ca6610908ae9
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Mar 01 17:45:19 2010 +0100
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Mar 01 21:41:35 2010 +0100
     1.3 @@ -286,14 +286,14 @@
     1.4  by auto
     1.5  
     1.6  lemma graph_implies_dom:
     1.7 -	"mrec_graph x y \<Longrightarrow> mrec_dom x"
     1.8 +  "mrec_graph x y \<Longrightarrow> mrec_dom x"
     1.9  apply (induct rule:mrec_graph.induct) 
    1.10  apply (rule accpI)
    1.11  apply (erule mrec_rel.cases)
    1.12  by simp
    1.13  
    1.14  lemma f_default: "\<not> mrec_dom (f, g, x, h) \<Longrightarrow> mrec f g x h = (Inr Exn, undefined)"
    1.15 -	unfolding mrec_def 
    1.16 +  unfolding mrec_def 
    1.17    by (rule fundef_default_value[OF mrec_sumC_def graph_implies_dom, of _ _ "(f, g, x, h)", simplified])
    1.18  
    1.19  lemma f_di_reverse: