changeset 23894 | 1a4167d761ac |
parent 20140 | 98acc6d0fab6 |
child 27221 | 31328dc30196 |
--- a/src/CCL/ex/Flag.thy Sat Jul 21 17:40:40 2007 +0200 +++ b/src/CCL/ex/Flag.thy Sat Jul 21 23:25:00 2007 +0200 @@ -56,7 +56,7 @@ unfolding ColourXH by blast+ ML {* -bind_thm ("ccaseT", mk_ncanT_tac (the_context ()) +bind_thm ("ccaseT", mk_ncanT_tac @{context} (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)"); *}