--- a/programs/prove2.scala	Tue Nov 12 10:51:02 2013 +0000
+++ b/programs/prove2.scala	Tue Nov 12 14:40:46 2013 +0000
@@ -1,5 +1,6 @@
 import scala.language.implicitConversions
 import scala.language.reflectiveCalls
+import scala.util._
 
 abstract class Term 
 case class Var(s: String) extends Term 
@@ -85,34 +86,32 @@
     case _ => ()
   }
 
-  
-
 // function that calls prove and returns immediately once a proof is found
 def run (j : Judgement) : Unit = {
-  try { 
-    def sc () = { println ("Yes!"); throw new Exception }
-    prove(j, sc) 
-  }
-  catch { case e: Exception => () }
+  def sc () = { println ("Yes!"); throw new Exception }
+  Try(prove(j, sc)) getOrElse ()
 } 
 
+run (goal)
+
 run (Set[Form]() |- False -> Del)
 run (Set[Form]() |- True -> Del)
 run (Set[Form]() |- Del -> True)
+run (Set[Form]() |- Del -> Del)
+run (Set[Form]() |- Del -> Or(False, Del))
 
-run (goal)
 
 val Gamma1 : Set[Form] = 
   Set( Admin says ((Bob says Del) -> Del),
        Bob says Del )
 
 val goal1 = Gamma1 |- Del // not provable
-
 run (goal1)
 
-run (Set[Form]() |- (Del -> Del))
 
-run (Set[Form]() |- (Del -> Or(False, Del)))
+val f1 = Pred("F1", Nil)
+val f2 = Pred("F2", Nil)
+run (Set[Form](And(f1, f2)) |- And(f2, f1))
 
 
 val Chr = "Christian"