diff -r 5fe67e108651 -r de6285ebcc05 src/HOL/Nitpick_Examples/Record_Nits.thy
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nitpick_Examples/Record_Nits.thy Fri Oct 23 18:59:24 2009 +0200
@@ -0,0 +1,84 @@
+(* Title: HOL/Nitpick_Examples/Record_Nits.thy
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2009
+
+Examples featuring Nitpick applied to records.
+*)
+
+header {* Examples Featuring Nitpick Applied to Records *}
+
+theory Record_Nits
+imports Main
+begin
+
+record point2d =
+ xc :: int
+ yc :: int
+
+lemma "\xc = x, yc = y\ = p\xc := x, yc := y\"
+nitpick [expect = none]
+sorry
+
+lemma "\xc = x, yc = y\ = p\xc := x\"
+nitpick [expect = genuine]
+oops
+
+lemma "p\xc := x, yc := y\ \ p"
+nitpick [expect = genuine]
+oops
+
+lemma "p\xc := x, yc := y\ = p"
+nitpick [expect = genuine]
+oops
+
+record point3d = point2d +
+ zc :: int
+
+lemma "\xc = x, yc = y, zc = z\ = p\xc := x, yc := y, zc := z\"
+nitpick [expect = none]
+sorry
+
+lemma "\xc = x, yc = y, zc = z\ = p\xc := x\"
+nitpick [expect = genuine]
+oops
+
+lemma "\xc = x, yc = y, zc = z\ = p\zc := z\"
+nitpick [expect = genuine]
+oops
+
+lemma "p\xc := x, yc := y, zc := z\ \ p"
+nitpick [expect = genuine]
+oops
+
+lemma "p\xc := x, yc := y, zc := z\ = p"
+nitpick [expect = genuine]
+oops
+
+record point4d = point3d +
+ wc :: int
+
+lemma "\xc = x, yc = y, zc = z, wc = w\ = p\xc := x, yc := y, zc := z, wc := w\"
+nitpick [expect = none]
+sorry
+
+lemma "\xc = x, yc = y, zc = z, wc = w\ = p\xc := x\"
+nitpick [expect = genuine]
+oops
+
+lemma "\xc = x, yc = y, zc = z, wc = w\ = p\zc := z\"
+nitpick [expect = genuine]
+oops
+
+lemma "\xc = x, yc = y, zc = z, wc = w\ = p\wc := w\"
+nitpick [expect = genuine]
+oops
+
+lemma "p\xc := x, yc := y, zc := z, wc := w\ \ p"
+nitpick [expect = genuine]
+oops
+
+lemma "p\xc := x, yc := y, zc := z, wc := w\ = p"
+nitpick [expect = genuine]
+oops
+
+end