Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use Main;
authorwenzelm
Thu, 06 Dec 2001 00:46:24 +0100
changeset 12406 c9775847ed66
parent 12405 9b16f99fd7b9
child 12407 70ebb59264f1
use Main;
src/HOL/Subst/AList.thy file | annotate | diff | comparison | revisions
src/HOL/Subst/UTerm.thy file | annotate | diff | comparison | revisions
src/HOL/Subst/Unify.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Subst/AList.thy	Thu Dec 06 00:45:04 2001 +0100
+++ b/src/HOL/Subst/AList.thy	Thu Dec 06 00:46:24 2001 +0100
@@ -6,7 +6,7 @@
 Association lists.
 *)
 
-AList = List + 
+AList = Main +
 
 consts
   alist_rec  :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
--- a/src/HOL/Subst/UTerm.thy	Thu Dec 06 00:45:04 2001 +0100
+++ b/src/HOL/Subst/UTerm.thy	Thu Dec 06 00:46:24 2001 +0100
@@ -7,7 +7,7 @@
 Binary trees with leaves that are constants or variables.
 *)
 
-UTerm = Finite + Datatype +
+UTerm = Main +
 
 datatype 'a uterm = Var ('a) 
                   | Const ('a)
--- a/src/HOL/Subst/Unify.thy	Thu Dec 06 00:45:04 2001 +0100
+++ b/src/HOL/Subst/Unify.thy	Thu Dec 06 00:46:24 2001 +0100
@@ -6,7 +6,7 @@
 Unification algorithm
 *)
 
-Unify = Unifier + Recdef + Option +
+Unify = Unifier +
 
 consts
isabelle