--- a/Fahad/CodeSamples/SequenceComprehensions.scala	Wed Nov 12 12:24:26 2014 +0000
+++ b/Fahad/CodeSamples/SequenceComprehensions.scala	Tue Dec 09 16:17:41 2014 +0000
@@ -1,3 +1,17 @@
+
+case class Twice(i: Int) {                              
+  def apply(x: Int, y: Int): Int = x * y
+  //def unapply(z: Int): Option[Int] = if (z % 2 == 0) Some(z/2) else None
+}
+
+Twice(21) match {
+  case Twice(n) => println(n)
+}
+
+Twice(21, 3) match {
+  case Twice(n) => println(n)
+}
+
 
 package Main
 
@@ -26,4 +40,4 @@
     i <- Iterator.range(0, 20);
     j <- Iterator.range(i + 1, 20) if i + j == 32
   ) println("(" + i + ", " + j + ")")
-}
\ No newline at end of file
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/Pr.thy	Tue Dec 09 16:17:41 2014 +0000
@@ -0,0 +1,43 @@
+theory Pr
+imports Main "~~/src/HOL/Number_Theory/Primes" "~~/src/HOL/Real"
+begin
+
+lemma 
+  fixes a b::nat
+  shows "(a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2"
+apply(simp add: power2_sum)
+done
+
+lemma
+  fixes a b c::"real"
+  assumes eq: "a * c \<le> b * c" and ineq: "b < a"
+  shows "c \<le> 0"
+proof -
+  {
+    assume  "0 < c" 
+    then have "b * c < a * c" using ineq by(auto)
+    then have "False" using eq by auto
+  } then show "c \<le> 0" by (auto simp add: not_le[symmetric]) 
+qed
+    
+
+
+
+lemma "n > 1 \<Longrightarrow> \<not>(prime (2 * n))"
+by (metis One_nat_def Suc_leI less_Suc0 not_le numeral_eq_one_iff prime_product semiring_norm(85))
+
+
+
+lemma 
+ fixes n::"nat"
+ assumes a: "n > 1"
+    and  b: "\<not>(prime n)"
+ shows "\<not>(prime ((2 ^ n) - 1))"   
+using a b
+apply(induct n)
+apply(simp)
+apply(simp)
+
+
+
+end
\ No newline at end of file