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.
bind_thms basic_monos;
authorwenzelm
Thu, 21 Feb 2002 20:10:05 +0100
changeset 12921 b7b0daf0d882
parent 12920 32292d83367b
child 12922 ed70a600f0ea
bind_thms basic_monos;
src/HOL/Sum_Type.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Sum_Type.ML	Thu Feb 21 20:09:48 2002 +0100
+++ b/src/HOL/Sum_Type.ML	Thu Feb 21 20:10:05 2002 +0100
@@ -159,7 +159,7 @@
 by (Blast_tac 1);
 qed "Part_mono";
 
-val basic_monos = basic_monos @ [Part_mono];
+bind_thms ("basic_monos", basic_monos @ [Part_mono]);
 
 Goalw [Part_def] "a : Part A h ==> a : A";
 by (etac IntD1 1);
isabelle