author haftmann Fri Jun 30 12:03:21 2006 +0200 (2006-06-30) changeset 19965 75a15223e21f parent 19964 73704ba4bed1 child 19966 88bbe97ed0b0
small change in class_package
```     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
```