src/HOL/Isar_examples/NestedDatatype.thy
changeset 18460 9a1458cb2956
parent 18153 a084aa91f701
child 23373 ead82c82da9e
     1.1 --- a/src/HOL/Isar_examples/NestedDatatype.thy	Thu Dec 22 00:28:41 2005 +0100
     1.2 +++ b/src/HOL/Isar_examples/NestedDatatype.thy	Thu Dec 22 00:28:43 2005 +0100
     1.3 @@ -27,10 +27,9 @@
     1.4   \medskip A simple lemma about composition of substitutions.
     1.5  *}
     1.6  
     1.7 -lemma
     1.8 -   "subst_term (subst_term f1 o f2) t =
     1.9 -      subst_term f1 (subst_term f2 t) &
    1.10 -    subst_term_list (subst_term f1 o f2) ts =
    1.11 +lemma "subst_term (subst_term f1 o f2) t =
    1.12 +      subst_term f1 (subst_term f2 t)"
    1.13 +  and "subst_term_list (subst_term f1 o f2) ts =
    1.14        subst_term_list f1 (subst_term_list f2 ts)"
    1.15    by (induct t and ts) simp_all
    1.16