src/HOL/BNF_Examples/Derivation_Trees/DTree.thy
changeset 55943 5c2df04e97d1
parent 55938 f20d1db5aa3c
child 57983 6edc3529bb4e
     1.1 --- a/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy	Thu Mar 06 15:14:09 2014 +0100
     1.2 +++ b/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy	Thu Mar 06 15:25:21 2014 +0100
     1.3 @@ -67,7 +67,7 @@
     1.4  lemma dtree_coinduct[elim, consumes 1, case_names Lift, induct pred: "HOL.eq"]:
     1.5  assumes phi: "\<phi> tr1 tr2" and
     1.6  Lift: "\<And> tr1 tr2. \<phi> tr1 tr2 \<Longrightarrow>
     1.7 -                  root tr1 = root tr2 \<and> rel_set (sum_rel op = \<phi>) (cont tr1) (cont tr2)"
     1.8 +                  root tr1 = root tr2 \<and> rel_set (rel_sum op = \<phi>) (cont tr1) (cont tr2)"
     1.9  shows "tr1 = tr2"
    1.10  using phi apply(elim dtree.coinduct)
    1.11  apply(rule Lift[unfolded rel_set_cont]) .