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.
Adapted to new inductive package.
authorberghofe
Tue, 30 Jun 1998 20:50:34 +0200
changeset 5101 52e7c75acfe6
parent 5100 68775c0e40e7
child 5102 8c782c25a11e
Adapted to new inductive package.
src/HOL/Finite.thy file | annotate | diff | comparison | revisions
src/HOL/Sexp.thy file | annotate | diff | comparison | revisions 
--- 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
 
--- 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
isabelle