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.
declare sym [elim?] in HOL.ML instead of Calculation.thy;
authorwenzelm
Thu, 19 Oct 2000 21:20:53 +0200
changeset 10273 59570adf2d3c
parent 10272 c02171c5fb20
child 10274 130ff5eb2b80
declare sym [elim?] in HOL.ML instead of Calculation.thy;
src/HOL/Calculation.thy file | annotate | diff | comparison | revisions
src/HOL/HOL.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Calculation.thy	Thu Oct 19 21:20:07 2000 +0200
+++ b/src/HOL/Calculation.thy	Thu Oct 19 21:20:53 2000 +0200
@@ -188,6 +188,4 @@
   trans
   transitive
 
-lemmas [elim?] = sym
-
 end
--- a/src/HOL/HOL.ML	Thu Oct 19 21:20:07 2000 +0200
+++ b/src/HOL/HOL.ML	Thu Oct 19 21:20:53 2000 +0200
@@ -32,6 +32,6 @@
 end;
 
 AddXIs [equal_intr_rule, disjI1, disjI2, ext];
-AddXEs [ex1_implies_ex, someI_ex];
+AddXEs [ex1_implies_ex, someI_ex, sym];
 
 open HOL;
isabelle