# HG changeset patch
# User berghofe
# Date 899232634 -7200
# Node ID 52e7c75acfe64437884e2bb9a52f9d8112e57869
# Parent  68775c0e40e70a691b730add52725a81d658860a
Adapted to new inductive package.

diff -r 68775c0e40e7 -r 52e7c75acfe6 src/HOL/Finite.thy
--- a/src/HOL/Finite.thy	Tue Jun 30 20:49:49 1998 +0200
+++ b/src/HOL/Finite.thy	Tue Jun 30 20:50:34 1998 +0200
@@ -6,7 +6,7 @@
 Finite sets and their cardinality
 *)
 
-Finite = Divides + Power + 
+Finite = Divides + Power + Inductive +
 
 consts Finites :: 'a set set
 
diff -r 68775c0e40e7 -r 52e7c75acfe6 src/HOL/Sexp.thy
--- a/src/HOL/Sexp.thy	Tue Jun 30 20:49:49 1998 +0200
+++ b/src/HOL/Sexp.thy	Tue Jun 30 20:50:34 1998 +0200
@@ -6,7 +6,7 @@
 S-expressions, general binary trees for defining recursive data structures
 *)
 
-Sexp = Univ +
+Sexp = Univ + Inductive +
 consts
   sexp      :: 'a item set