src/HOL/Subst/Unifier.thy
changeset 1374 5e407f2a3323
parent 1151 c820b3cc3df0
child 1476 608483c2122a
     1.1 --- a/src/HOL/Subst/Unifier.thy	Wed Nov 29 16:58:30 1995 +0100
     1.2 +++ b/src/HOL/Subst/Unifier.thy	Wed Nov 29 17:01:41 1995 +0100
     1.3 @@ -14,7 +14,7 @@
     1.4    ">>"       :: "[('a*('a uterm))list,('a*('a uterm))list] => bool" (infixr 52)
     1.5    MGUnifier  :: "[('a*('a uterm))list,'a uterm,'a uterm] => bool"
     1.6    MGIUnifier :: "[('a*('a uterm))list,'a uterm,'a uterm] => bool"
     1.7 -  UWFD       :: "['a uterm,'a uterm,'a uterm,'a uterm] => bool"
     1.8 +  UWFD       :: ['a uterm,'a uterm,'a uterm,'a uterm] => bool
     1.9  
    1.10  rules  (*Definitions*)
    1.11