src/HOL/ex/Classpackage.thy
changeset 19965 75a15223e21f
parent 19958 fc4ac94f03e0
child 20106 a3d4b4eb35b9
     1.1 --- a/src/HOL/ex/Classpackage.thy	Thu Jun 29 18:11:15 2006 +0200
     1.2 +++ b/src/HOL/ex/Classpackage.thy	Fri Jun 30 12:03:21 2006 +0200
     1.3 @@ -61,8 +61,8 @@
     1.4    fix xs :: "'a list"
     1.5    show "\<one> \<otimes> xs = xs"
     1.6    proof -
     1.7 -    from semigroup_list_def have "\<And>xs ys::'a list. xs \<otimes> ys == xs @ ys".
     1.8 -    moreover from monoidl_list_def have "\<one> == []::'a list".
     1.9 +    from semigroup_list_def have "\<And>xs ys::'a list. xs \<otimes> ys == xs @ ys" .
    1.10 +    moreover from monoidl_list_def have "\<one> == []::'a list" by simp
    1.11      ultimately show ?thesis by simp
    1.12    qed
    1.13  qed  
    1.14 @@ -75,8 +75,8 @@
    1.15    fix xs :: "'a list"
    1.16    show "xs \<otimes> \<one> = xs"
    1.17    proof -
    1.18 -    from semigroup_list_def have "\<And>xs ys::'a list. xs \<otimes> ys == xs @ ys".
    1.19 -    moreover from monoidl_list_def have "\<one> == []::'a list".
    1.20 +    from semigroup_list_def have "\<And>xs ys::'a list. xs \<otimes> ys == xs @ ys" .
    1.21 +    moreover from monoidl_list_def have "\<one> == []::'a list" by simp
    1.22      ultimately show ?thesis by simp
    1.23    qed
    1.24  qed