Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
(simp add: point.make_def);
authorwenzelm
Thu, 25 Oct 2001 02:11:49 +0200
changeset 11928 d0bae2c3abad
parent 11927 96f267adc029
child 11929 a77ad6c86564
(simp add: point.make_def);
src/HOL/ex/Records.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle