--- 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
--- 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"
--- 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"
--- 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 *)