merged
authorwenzelm
Sat, 25 Jun 2011 14:28:43 +0200
changeset 43544 6b95bcc5c2da
parent 43543 eb8b4851b039 (current diff)
parent 43542 7e2ef426c960 (diff)
child 43545 1cf2256f1b07
merged
Isabelle.exe
--- 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());
   }
 }