# HG changeset patch
# User wenzelm
# Date 1329408555 -3600
# Node ID cefceb54c6565597812d6f1fe2155b4ba331b38d
# Parent  cd4832aa22293466212ecb57754db6e82fdeec7f# Parent  186f4cab2ba09910b4a5fa586445183120a8eecc
merged

diff -r cd4832aa2229 -r cefceb54c656 src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Thu Feb 16 16:02:02 2012 +0100
+++ b/src/HOL/Tools/Meson/meson.ML	Thu Feb 16 17:09:15 2012 +0100
@@ -756,8 +756,8 @@
 (*Rules to convert the head literal into a negated assumption. If the head
   literal is already negated, then using notEfalse instead of notEfalse'
   prevents a double negation.*)
-val notEfalse = read_instantiate @{context} [(("R", 0), "False")] notE;
-val notEfalse' = rotate_prems 1 notEfalse;
+val notEfalse = @{lemma "~ P ==> P ==> False" by (rule notE)};
+val notEfalse' = @{lemma "P ==> ~ P ==> False" by (rule notE)};
 
 fun negated_asm_of_head th =
     th RS notEfalse handle THM _ => th RS notEfalse';
diff -r cd4832aa2229 -r cefceb54c656 src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Thu Feb 16 16:02:02 2012 +0100
+++ b/src/Pure/System/isabelle_system.ML	Thu Feb 16 17:09:15 2012 +0100
@@ -62,7 +62,7 @@
 
 fun copy_dir src dst =
   if File.eq (src, dst) then ()
-  else (system_command ("cp -r -f " ^ File.shell_path src ^ "/. " ^ File.shell_path dst); ());
+  else (system_command ("cp -p -R -f " ^ File.shell_path src ^ "/. " ^ File.shell_path dst); ());
 
 
 (* unique tmp files *)
diff -r cd4832aa2229 -r cefceb54c656 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Thu Feb 16 16:02:02 2012 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Thu Feb 16 17:09:15 2012 +0100
@@ -223,11 +223,11 @@
   rm -rf dist || failed
   mkdir -p dist dist/classes || failed
 
-  cp -pR "$ISABELLE_JEDIT_BUILD_HOME/contrib/$ISABELLE_JEDIT_BUILD_VERSION/." dist/.
-  cp -pR "${RESOURCES[@]}" dist/classes/.
+  cp -p -R -f "$ISABELLE_JEDIT_BUILD_HOME/contrib/$ISABELLE_JEDIT_BUILD_VERSION/." dist/.
+  cp -p -R -f "${RESOURCES[@]}" dist/classes/.
   cp src/jEdit.props dist/properties/.
-  cp -pR src/modes/. dist/modes/.
-  cp -pR "$SCALA_HOME/misc/scala-tool-support/jedit/modes/scala.xml" dist/modes/.
+  cp -p -R -f src/modes/. dist/modes/.
+  cp -p -R -f "$SCALA_HOME/misc/scala-tool-support/jedit/modes/scala.xml" dist/modes/.
 
   perl -i -e 'while (<>) {
     if (m/NAME="javacc"/) {
@@ -237,7 +237,7 @@
       print qq,<MODE NAME="scala" FILE="scala.xml" FILE_NAME_GLOB="*.scala" />\n\n,; }
     print; }' dist/modes/catalog
 
-  cp -pR "${JEDIT_JARS[@]}" "$SCALA_HOME/lib/scala-compiler.jar" dist/jars/. || failed
+  cp -p -R -f "${JEDIT_JARS[@]}" "$SCALA_HOME/lib/scala-compiler.jar" dist/jars/. || failed
   (
     for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "$SCALA_HOME/lib/scala-compiler.jar"
     do