--- a/src/Tools/Metis/src/Rule.sig Mon Sep 13 16:44:20 2010 +0200
+++ b/src/Tools/Metis/src/Rule.sig Mon Sep 13 21:24:10 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* DERIVED RULES FOR CREATING FIRST ORDER LOGIC THEOREMS *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Rule =
@@ -13,7 +13,7 @@
type equation = (Term.term * Term.term) * Thm.thm
-val ppEquation : equation Parser.pp
+val ppEquation : equation Print.pp
val equationToString : equation -> string
@@ -143,6 +143,8 @@
(* x = x *)
(* ------------------------------------------------------------------------- *)
+val reflexivityRule : Term.term -> Thm.thm
+
val reflexivity : Thm.thm
(* ------------------------------------------------------------------------- *)
@@ -151,6 +153,8 @@
(* ~(x = y) \/ y = x *)
(* ------------------------------------------------------------------------- *)
+val symmetryRule : Term.term -> Term.term -> Thm.thm
+
val symmetry : Thm.thm
(* ------------------------------------------------------------------------- *)