src/HOL/BNF/Examples/Derivation_Trees/DTree.thy
changeset 55066 4e5ddf3162ac
parent 54625 f312a035d0cf
     1.1 --- a/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy	Mon Jan 20 18:24:56 2014 +0100
     1.2 +++ b/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy	Mon Jan 20 18:24:56 2014 +0100
     1.3 @@ -24,11 +24,11 @@
     1.4  definition "corec rt ct \<equiv> corec_dtree rt (the_inv fset o ct)"
     1.5  
     1.6  lemma finite_cont[simp]: "finite (cont tr)"
     1.7 -  unfolding cont_def o_apply by (cases tr, clarsimp)
     1.8 +  unfolding cont_def comp_apply by (cases tr, clarsimp)
     1.9  
    1.10  lemma Node_root_cont[simp]:
    1.11    "Node (root tr) (cont tr) = tr"
    1.12 -  unfolding Node_def cont_def o_apply
    1.13 +  unfolding Node_def cont_def comp_apply
    1.14    apply (rule trans[OF _ dtree.collapse])
    1.15    apply (rule arg_cong2[OF refl the_inv_into_f_f[unfolded inj_on_def]])
    1.16    apply (simp_all add: fset_inject)