# HG changeset patch
# User blanchet
# Date 1292936239 -3600
# Node ID 7e82d621adc651aeeacb56f34025ee292d2a6b84
# Parent  1eefe189434a3ddd9ebe205137ed68a3ef80fe04
show the relation

diff -r 1eefe189434a -r 7e82d621adc6 src/HOL/Nitpick_Examples/Hotel_Nits.thy
--- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Tue Dec 21 10:25:17 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Tue Dec 21 13:57:19 2010 +0100
@@ -51,7 +51,8 @@
 
 theorem safe: "s \<in> reach \<Longrightarrow> safe s r \<Longrightarrow> g \<in> isin s r \<Longrightarrow> owns s r = Some g"
 nitpick [card room = 1, card guest = 2, card "guest option" = 3,
-         card key = 4, card state = 6, expect = genuine]
+         card key = 4, card state = 6, show_consts, format = 2,
+         expect = genuine]
 (* nitpick [card room = 1, card guest = 2, expect = genuine] *)
 oops