diff -r 8b44bd114292 -r 93578c484ab1 programs/prove1.scala
--- a/programs/prove1.scala	Tue Oct 30 07:11:42 2012 +0000
+++ b/programs/prove1.scala	Tue Oct 30 14:27:59 2012 +0000
@@ -1,10 +1,12 @@
 
-abstract class Term
+abstract class Term 
 case class Var(s: String) extends Term 
 case class Const(s: String) extends Term 
 case class Fun(s: String, ts: List[Term]) extends Term
 
-abstract class Form
+abstract class Form {
+  def -> (that: Form) = Imp(this, that)
+}
 case object True extends Form
 case object False extends Form
 case class Pred(s: String, ts: List[Term]) extends Form
@@ -24,8 +26,8 @@
 
 
 val Gamma = 
-  List( Imp(Says(Admin, Del), Del),
-        Says(Admin, Imp(Says(Bob, Del), Del)),
+  List( Says(Admin, Del) -> Del,
+        Says(Admin, Says(Bob, Del) -> Del),
         Says(Bob, Del) )
 
 val goal = Judgement(Gamma, Del) // request: provable or not?
@@ -82,7 +84,7 @@
 run (goal)
 
 
-run (Judgement(Nil, Imp(Del, Del)))
+run (Judgement(Nil, Del -> Del))
 
 val Chr = "Christian"
 val HoD = "Michael Luck"
@@ -90,8 +92,8 @@
 val AtLib = Pred("is_at_library", List(Const(Chr)))
 val Chr_Staff = Pred("is_staff", List(Const(Chr)))
 
-val Policy_HoD = Imp(Says(HoD, Chr_Staff), Chr_Staff)
-val Policy_Lib = Imp(And(Chr_Staff, AtLib), Email)
+val Policy_HoD = Says(HoD, Chr_Staff) -> Chr_Staff
+val Policy_Lib = And(Chr_Staff, AtLib) -> Email
 val HoD_says = Says(HoD, Chr_Staff)
 
 run (Judgement (List(AtLib, Policy_HoD, Policy_Lib, HoD_says), Email))