--- a/Isabelle Sat Jun 25 12:19:54 2011 +0200
+++ b/Isabelle Sat Jun 25 14:28:43 2011 +0200
@@ -23,7 +23,6 @@
[ -e "$ISABELLE_HOME/Admin/build" ] && "$ISABELLE_HOME/Admin/build" jars
-CLASSPATH="$(jvmpath "$CLASSPATH")"
exec "$ISABELLE_TOOL" java \
"-Disabelle.home=$(jvmpath "$ISABELLE_HOME")" \
isabelle.GUI_Setup "$@"
Binary file Isabelle.exe has changed
--- a/src/HOL/Quickcheck_Narrowing.thy Sat Jun 25 12:19:54 2011 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy Sat Jun 25 14:28:43 2011 +0200
@@ -384,44 +384,6 @@
by (simp add: around_zero.simps[of "i + 1"])
qed
-lemma
- assumes "int n <= 2 * i"
- shows "(n mod 2 = 1 --> around_zero i ! n = (int n + 1) div 2) &
- (n mod 2 = 0 --> around_zero i ! n = (- (int n)) div 2)"
-using assms
-proof (cases "i >= 0")
- case False
- with assms show ?thesis by (simp add: around_zero.simps[of i])
-next
- case True
- from assms show ?thesis
- proof (induct rule: int_ge_induct[OF True])
- case (2 i)
- have i: "n < Suc (2 * nat i) \<or> n = Suc (2 * nat i) \<or> n = (2 * nat i) + 2 \<or> n > (2 * nat i) + 2"
- by arith
- show ?case
- proof -
- {
- assume "n mod 2 = 1"
- from 2 length_around_zero[OF 2(1)] this i have "around_zero (i + 1) ! n = (int n + 1) div 2"
- unfolding around_zero.simps[of "i + 1"]
- by (auto simp add: nth_append)
- } moreover
- {
- assume a: "n mod 2 = 0"
- have "\<forall> q q'. 2 * q \<noteq> Suc (2 * q')" by arith
- from a 2 length_around_zero[OF 2(1)] this i have "around_zero (i + 1) ! n = - int n div 2"
- unfolding around_zero.simps[of "i + 1"]
- by (auto simp add: nth_append)
- }
- ultimately show ?thesis by auto
- qed
- next
- case 1
- from 1 show ?case by (auto simp add: around_zero.simps[of 0])
- qed
-qed
-
instantiation int :: narrowing
begin
--- a/src/Pure/System/Java_Ext_Dirs.java Sat Jun 25 12:19:54 2011 +0200
+++ b/src/Pure/System/Java_Ext_Dirs.java Sat Jun 25 14:28:43 2011 +0200
@@ -10,12 +10,12 @@
{
public static void main(String [] args) {
StringBuilder s = new StringBuilder();
- s.append(System.getProperty("java.ext.dirs"));
int i;
for (i = 0; i < args.length; i++) {
+ s.append(args[i]);
s.append(System.getProperty("path.separator"));
- s.append(args[i]);
}
+ s.append(System.getProperty("java.ext.dirs"));
System.out.println(s.toString());
}
}