| changeset 28272 | ed959a0f650b |
| parent 27221 | 31328dc30196 |
| child 32153 | a0e57fb1b930 |
--- a/src/CCL/ex/Flag.thy Wed Sep 17 21:27:34 2008 +0200 +++ b/src/CCL/ex/Flag.thy Wed Sep 17 21:27:36 2008 +0200 @@ -57,7 +57,7 @@ ML {* bind_thm ("ccaseT", mk_ncanT_tac @{context} - (thms "flag_defs") (thms "case_rls") (thms "case_rls") + @{thms flag_defs} @{thms case_rls} @{thms case_rls} "[| c:Colour; c=red ==> r : C(red); c=white ==> w : C(white); c=blue ==> b : C(blue) |] ==> ccase(c,r,w,b) : C(c)"); *}