diff -r f04b33ce250f -r a4dc62a46ee4 Subst/Unifier.thy
--- a/Subst/Unifier.thy	Tue Oct 24 14:59:17 1995 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-(*  Title: 	Subst/unifier.thy
-    Author: 	Martin Coen, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
-
-Definition of most general idempotent unifier
-*)
-
-Unifier = Subst +
-
-consts
-
-  Idem       :: "('a*('a uterm))list=> bool"
-  Unifier    :: "[('a*('a uterm))list,'a uterm,'a uterm] => bool"
-  ">>"       :: "[('a*('a uterm))list,('a*('a uterm))list] => bool" (infixr 52)
-  MGUnifier  :: "[('a*('a uterm))list,'a uterm,'a uterm] => bool"
-  MGIUnifier :: "[('a*('a uterm))list,'a uterm,'a uterm] => bool"
-  UWFD       :: "['a uterm,'a uterm,'a uterm,'a uterm] => bool"
-
-rules  (*Definitions*)
-
-  Idem_def         "Idem(s) == s <> s =s= s"
-  Unifier_def      "Unifier(s,t,u) == t <| s = u <| s"
-  MoreGeneral_def  "r >> s == ? q.s =s= r <> q"
-  MGUnifier_def    "MGUnifier(s,t,u) == Unifier(s,t,u) & 
-		    (! r.Unifier(r,t,u) --> s >> r)"
-  MGIUnifier_def   "MGIUnifier(s,t,u) == MGUnifier(s,t,u) & Idem(s)"
-
-  UWFD_def
-  "UWFD(x,y,x',y') == 
-    (vars_of(x) Un vars_of(y) < vars_of(x') Un vars_of(y')) |  
-    (vars_of(x) Un vars_of(y) = vars_of(x') Un vars_of(y') & x <: x')"
-
-end