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.
tuned declarations;
authorwenzelm
Wed, 28 Nov 2001 00:37:40 +0100
changeset 12304 8df202daf55d
parent 12303 67ca723a02dd
child 12305 3c3f98b3d9e7
tuned declarations;
src/HOL/Divides.ML file | annotate | diff | comparison | revisions
src/HOL/PreList.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Divides.ML	Wed Nov 28 00:37:08 2001 +0100
+++ b/src/HOL/Divides.ML	Wed Nov 28 00:37:40 2001 +0100
@@ -508,12 +508,10 @@
 Goalw [dvd_def] "n = m * k ==> m dvd n";
 by (Blast_tac 1); 
 qed "dvdI";
-AddXIs [dvdI];
 
 Goalw [dvd_def] "!!P. [|m dvd n;  !!k. n = m*k ==> P|] ==> P";
 by (Blast_tac 1); 
 qed "dvdE";
-AddXEs [dvdE];
 
 Goalw [dvd_def] "m dvd (0::nat)";
 by (blast_tac (claset() addIs [mult_0_right RS sym]) 1);
--- a/src/HOL/PreList.thy	Wed Nov 28 00:37:08 2001 +0100
+++ b/src/HOL/PreList.thy	Wed Nov 28 00:37:40 2001 +0100
@@ -12,7 +12,7 @@
   Relation_Power + SVC_Oracle:
 
 (*belongs to theory Divides*)
-declare dvd_trans [trans]
+declare dvdI [intro?]  dvdE [elim?]  dvd_trans [trans]
 
 (*belongs to theory Wellfounded_Recursion*)
 declare wf_induct [induct set: wf]
isabelle