src/HOL/ex/Records.thy
changeset 12266 fa0a3e95d395
parent 11939 c5e69470f03b
child 12591 5a46569d2b05
--- 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