use Main;
authorwenzelm
Thu Dec 06 00:46:24 2001 +0100 (2001-12-06)
changeset 12406c9775847ed66
parent 12405 9b16f99fd7b9
child 12407 70ebb59264f1
use Main;
src/HOL/Subst/AList.thy
src/HOL/Subst/UTerm.thy
src/HOL/Subst/Unify.thy
     1.1 --- a/src/HOL/Subst/AList.thy	Thu Dec 06 00:45:04 2001 +0100
     1.2 +++ b/src/HOL/Subst/AList.thy	Thu Dec 06 00:46:24 2001 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  Association lists.
     1.5  *)
     1.6  
     1.7 -AList = List + 
     1.8 +AList = Main +
     1.9  
    1.10  consts
    1.11    alist_rec  :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
     2.1 --- a/src/HOL/Subst/UTerm.thy	Thu Dec 06 00:45:04 2001 +0100
     2.2 +++ b/src/HOL/Subst/UTerm.thy	Thu Dec 06 00:46:24 2001 +0100
     2.3 @@ -7,7 +7,7 @@
     2.4  Binary trees with leaves that are constants or variables.
     2.5  *)
     2.6  
     2.7 -UTerm = Finite + Datatype +
     2.8 +UTerm = Main +
     2.9  
    2.10  datatype 'a uterm = Var ('a) 
    2.11                    | Const ('a)
     3.1 --- a/src/HOL/Subst/Unify.thy	Thu Dec 06 00:45:04 2001 +0100
     3.2 +++ b/src/HOL/Subst/Unify.thy	Thu Dec 06 00:46:24 2001 +0100
     3.3 @@ -6,7 +6,7 @@
     3.4  Unification algorithm
     3.5  *)
     3.6  
     3.7 -Unify = Unifier + Recdef + Option +
     3.8 +Unify = Unifier +
     3.9  
    3.10  consts
    3.11