# HG changeset patch
# User nipkow
# Date 1290791220 -3600
# Node ID 88f2955a111e0971250875b1fc13a0644a9ee718
# Parent  3ba17f07b23c241e6330c105ce026affd8a24e23# Parent  a92d744bca5f840a834a23cf4b0f7f3427c1c1ea
merged

diff -r a92d744bca5f -r 88f2955a111e Admin/makedist
--- a/Admin/makedist	Fri Nov 26 18:06:48 2010 +0100
+++ b/Admin/makedist	Fri Nov 26 18:07:00 2010 +0100
@@ -186,16 +186,13 @@
 echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST
 echo "$IDENT" >../ISABELLE_IDENT
 
-rm -f Isabelle
-ln -s "$DISTNAME" Isabelle
-
 chown -R "$LOGNAME" "$DISTNAME"
 chmod -R u+w "$DISTNAME"
 chmod -R g=o "$DISTNAME"
-chgrp -R isabelle "$DISTNAME" Isabelle
+chgrp -R isabelle "$DISTNAME"
 
 echo "$DISTNAME.tar.gz"
-tar -czf "$DISTNAME.tar.gz" Isabelle "$DISTNAME"
+tar -czf "$DISTNAME.tar.gz" "$DISTNAME"
 
 
 # cleanup dist
diff -r a92d744bca5f -r 88f2955a111e src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Fri Nov 26 18:06:48 2010 +0100
+++ b/src/HOL/Complete_Lattice.thy	Fri Nov 26 18:07:00 2010 +0100
@@ -528,7 +528,7 @@
   @{prop "X:C"} does not!  This rule is analogous to @{text spec}.
 *}
 
-lemma InterD [elim]: "A : Inter C ==> X:C ==> A:X"
+lemma InterD [elim, Pure.elim]: "A : Inter C ==> X:C ==> A:X"
   by auto
 
 lemma InterE [elim]: "A : Inter C ==> (X~:C ==> R) ==> (A:X ==> R) ==> R"
@@ -622,7 +622,7 @@
 lemma INT_I [intro!]: "(!!x. x:A ==> b: B x) ==> b : (INT x:A. B x)"
   by (unfold INTER_def) blast
 
-lemma INT_D [elim]: "b : (INT x:A. B x) ==> a:A ==> b: B a"
+lemma INT_D [elim, Pure.elim]: "b : (INT x:A. B x) ==> a:A ==> b: B a"
   by auto
 
 lemma INT_E [elim]: "b : (INT x:A. B x) ==> (b: B a ==> R) ==> (a~:A ==> R) ==> R"
diff -r a92d744bca5f -r 88f2955a111e src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Nov 26 18:06:48 2010 +0100
+++ b/src/HOL/HOL.thy	Fri Nov 26 18:07:00 2010 +0100
@@ -214,6 +214,9 @@
 lemma trans: "[| r=s; s=t |] ==> r=t"
   by (erule subst)
 
+lemma trans_sym [Pure.elim?]: "r = s ==> t = s ==> r = t"
+  by (rule trans [OF _ sym])
+
 lemma meta_eq_to_obj_eq: 
   assumes meq: "A == B"
   shows "A = B"
diff -r a92d744bca5f -r 88f2955a111e src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Fri Nov 26 18:06:48 2010 +0100
+++ b/src/ZF/ZF.thy	Fri Nov 26 18:07:00 2010 +0100
@@ -603,7 +603,7 @@
 
 (*A "destruct" rule -- every B in C contains A as an element, but
   A\<in>B can hold when B\<in>C does not!  This rule is analogous to "spec". *)
-lemma InterD [elim]: "[| A \<in> Inter(C);  B \<in> C |] ==> A \<in> B"
+lemma InterD [elim, Pure.elim]: "[| A \<in> Inter(C);  B \<in> C |] ==> A \<in> B"
 by (unfold Inter_def, blast)
 
 (*"Classical" elimination rule -- does not require exhibiting B\<in>C *)