src/HOL/BNF_Examples/Derivation_Trees/DTree.thy
changeset 57991 f50b3726266f
parent 57983 6edc3529bb4e
     1.1 --- a/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy	Tue Aug 19 09:34:27 2014 +0200
     1.2 +++ b/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy	Tue Aug 19 09:34:30 2014 +0200
     1.3 @@ -47,13 +47,13 @@
     1.4  using Node unfolding Node_def
     1.5  by (metis Node Node_root_cont finite_cont)
     1.6  
     1.7 -lemma dtree_sel_ctor[simp]:
     1.8 +lemma dtree_sel_ctr[simp]:
     1.9  "root (Node n as) = n"
    1.10  "finite as \<Longrightarrow> cont (Node n as) = as"
    1.11  unfolding Node_def cont_def by auto
    1.12  
    1.13 -lemmas root_Node = dtree_sel_ctor(1)
    1.14 -lemmas cont_Node = dtree_sel_ctor(2)
    1.15 +lemmas root_Node = dtree_sel_ctr(1)
    1.16 +lemmas cont_Node = dtree_sel_ctr(2)
    1.17  
    1.18  lemma dtree_cong:
    1.19  assumes "root tr = root tr'" and "cont tr = cont tr'"