src/HOL/Sexp.thy
changeset 5101 52e7c75acfe6
parent 1788 ca62fab4ce92
child 5191 8ceaa19f7717
     1.1 --- a/src/HOL/Sexp.thy	Tue Jun 30 20:49:49 1998 +0200
     1.2 +++ b/src/HOL/Sexp.thy	Tue Jun 30 20:50:34 1998 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  S-expressions, general binary trees for defining recursive data structures
     1.5  *)
     1.6  
     1.7 -Sexp = Univ +
     1.8 +Sexp = Univ + Inductive +
     1.9  consts
    1.10    sexp      :: 'a item set
    1.11