--- 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';
--- 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 *)
--- 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