src/HOL/Nitpick_Examples/Manual_Nits.thy
changeset 35711 548d3f16404b
parent 35710 58acd48904bc
child 35712 77aa29bf14ee
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Thu Mar 11 10:13:24 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Thu Mar 11 12:22:11 2010 +0100
@@ -117,6 +117,19 @@
 nitpick [show_datatypes, expect = genuine]
 oops
 
+ML {*
+(* Proof.context -> typ -> term -> term *)
+fun my_int_postproc _ T (Const _ $ (Const _ $ t1 $ t2)) =
+    HOLogic.mk_number T (snd (HOLogic.dest_number t1) - snd (HOLogic.dest_number t2))
+  | my_int_postproc _ _ t = t
+*}
+
+setup {* Nitpick.register_term_postprocessor @{typ my_int} my_int_postproc *}
+
+lemma "add x y = add x x"
+nitpick [show_datatypes]
+oops
+
 record point =
   Xcoord :: int
   Ycoord :: int