# 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,\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