# HG changeset patch
# User wenzelm
# Date 1006445604 -3600
# Node ID fa0a3e95d395513d9d288ca32a981ac9139c608d
# Parent  6df58e87ec91ef4cafb03afe4868b4bc326c4d75
thm "point.defs";

diff -r 6df58e87ec91 -r fa0a3e95d395 src/HOL/ex/Records.thy
--- a/src/HOL/ex/Records.thy	Thu Nov 22 17:13:06 2001 +0100
+++ b/src/HOL/ex/Records.thy	Thu Nov 22 17:13:24 2001 +0100
@@ -21,7 +21,7 @@
 
 thm "point.simps"
 thm "point.iffs"
-thm "point.derived_defs"
+thm "point.defs"
 
 text {*
   The set of theorems @{thm [source] point.simps} is added