# HG changeset patch
# User wenzelm
# Date 1003968709 -7200
# Node ID d0bae2c3abada16dc3599d2a77b538e4625ea491
# Parent  96f267adc0294ab29ad5d547d9ea2079a3a925a7
(simp add: point.make_def);

diff -r 96f267adc029 -r d0bae2c3abad src/HOL/ex/Records.thy
--- a/src/HOL/ex/Records.thy	Thu Oct 25 02:11:28 2001 +0200
+++ b/src/HOL/ex/Records.thy	Thu Oct 25 02:11:49 2001 +0200
@@ -64,7 +64,7 @@
 text {* Basic simplifications. *}
 
 lemma "point.make n p = (| x = n, y = p |)"
-  by simp
+  by (simp add: point.make_def)
 
 lemma "x (| x = m, y = n, ... = p |) = m"
   by simp