# HG changeset patch
# User paulson
# Date 991326503 -7200
# Node ID 9b80fe19407fcbdab5058cdedf8244c920fab11f
# Parent  7f6eff7bc97af22528515cd0c019cda1bd975bb3
examples files start from Main instead of various ZF theories

diff -r 7f6eff7bc97a -r 9b80fe19407f src/ZF/Coind/Language.thy
--- a/src/ZF/Coind/Language.thy	Thu May 31 17:57:02 2001 +0200
+++ b/src/ZF/Coind/Language.thy	Thu May 31 18:28:23 2001 +0200
@@ -4,11 +4,11 @@
     Copyright   1995  University of Cambridge
 *)
 
-Language = Datatype + QUniv +
+Language = Main +
 
 consts
   Const :: i                    (* Abstract type of constants *)
-  c_app :: [i,i] => i           (*Abstract constructor for fun application*)
+  c_app :: [i,i] => i           (* Abstract constructor for fun application*)
 
 rules
   constNEE  "c \\<in> Const ==> c \\<noteq> 0"
diff -r 7f6eff7bc97a -r 9b80fe19407f src/ZF/Coind/Map.thy
--- a/src/ZF/Coind/Map.thy	Thu May 31 17:57:02 2001 +0200
+++ b/src/ZF/Coind/Map.thy	Thu May 31 18:28:23 2001 +0200
@@ -4,7 +4,7 @@
     Copyright   1995  University of Cambridge
 *)
 
-Map = QUniv +
+Map = Main +
 
 constdefs
   TMap :: [i,i] => i
diff -r 7f6eff7bc97a -r 9b80fe19407f src/ZF/ex/Acc.thy
--- a/src/ZF/ex/Acc.thy	Thu May 31 17:57:02 2001 +0200
+++ b/src/ZF/ex/Acc.thy	Thu May 31 18:28:23 2001 +0200
@@ -9,7 +9,7 @@
 Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
 *)
 
-Acc = WF + Inductive +
+Acc = Main +
 
 consts
   acc :: i=>i
diff -r 7f6eff7bc97a -r 9b80fe19407f src/ZF/ex/Brouwer.thy
--- a/src/ZF/ex/Brouwer.thy	Thu May 31 17:57:02 2001 +0200
+++ b/src/ZF/ex/Brouwer.thy	Thu May 31 18:28:23 2001 +0200
@@ -8,7 +8,8 @@
   (2) the Martin-Löf wellordering type
 *)
 
-Brouwer = InfDatatype +
+Brouwer = Main +
+
 consts
   brouwer :: i
   Well    :: [i,i=>i]=>i
diff -r 7f6eff7bc97a -r 9b80fe19407f src/ZF/ex/CoUnit.thy
--- a/src/ZF/ex/CoUnit.thy	Thu May 31 17:57:02 2001 +0200
+++ b/src/ZF/ex/CoUnit.thy	Thu May 31 18:28:23 2001 +0200
@@ -10,7 +10,7 @@
   Report 334,  Cambridge University Computer Laboratory.  1994.
 *)
 
-CoUnit = Datatype +
+CoUnit = Main +
 
 (*This degenerate definition does not work well because the one constructor's
   definition is trivial!  The same thing occurs with Aczel's Special Final
diff -r 7f6eff7bc97a -r 9b80fe19407f src/ZF/ex/Comb.thy
--- a/src/ZF/ex/Comb.thy	Thu May 31 17:57:02 2001 +0200
+++ b/src/ZF/ex/Comb.thy	Thu May 31 18:28:23 2001 +0200
@@ -13,7 +13,7 @@
 *)
 
 
-Comb = Datatype +
+Comb = Main +
 
 (** Datatype definition of combinators S and K, with infixed application **)
 consts comb :: i
diff -r 7f6eff7bc97a -r 9b80fe19407f src/ZF/ex/Data.thy
--- a/src/ZF/ex/Data.thy	Thu May 31 17:57:02 2001 +0200
+++ b/src/ZF/ex/Data.thy	Thu May 31 18:28:23 2001 +0200
@@ -7,7 +7,7 @@
 It has four contructors, of arities 0-3, and two parameters A and B.
 *)
 
-Data = Datatype +
+Data = Main +
 
 consts
   data :: [i,i] => i
diff -r 7f6eff7bc97a -r 9b80fe19407f src/ZF/ex/Enum.thy
--- a/src/ZF/ex/Enum.thy	Thu May 31 17:57:02 2001 +0200
+++ b/src/ZF/ex/Enum.thy	Thu May 31 18:28:23 2001 +0200
@@ -8,7 +8,7 @@
 Can go up to at least 100 constructors, but it takes nearly 7 minutes...
 *)
 
-Enum = Datatype + 
+Enum = Main + 
 
 consts
   enum :: i
diff -r 7f6eff7bc97a -r 9b80fe19407f src/ZF/ex/LList.thy
--- a/src/ZF/ex/LList.thy	Thu May 31 17:57:02 2001 +0200
+++ b/src/ZF/ex/LList.thy	Thu May 31 18:28:23 2001 +0200
@@ -14,7 +14,7 @@
 a typing rule for it, based on some notion of "productivity..."
 *)
 
-LList = Datatype +
+LList = Main +
 
 consts
   llist  :: i=>i
diff -r 7f6eff7bc97a -r 9b80fe19407f src/ZF/ex/ListN.thy
--- a/src/ZF/ex/ListN.thy	Thu May 31 17:57:02 2001 +0200
+++ b/src/ZF/ex/ListN.thy	Thu May 31 18:28:23 2001 +0200
@@ -9,7 +9,8 @@
 Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
 *)
 
-ListN = List +
+ListN = Main +
+
 consts  listn ::i=>i
 inductive
   domains   "listn(A)" <= "nat*list(A)"
@@ -17,4 +18,5 @@
     NilI  "<0,Nil> \\<in> listn(A)"
     ConsI "[| a \\<in> A; <n,l> \\<in> listn(A) |] ==> <succ(n), Cons(a,l)> \\<in> listn(A)"
   type_intrs "nat_typechecks @ list.intrs"
+
 end
diff -r 7f6eff7bc97a -r 9b80fe19407f src/ZF/ex/Mutil.thy
--- a/src/ZF/ex/Mutil.thy	Thu May 31 17:57:02 2001 +0200
+++ b/src/ZF/ex/Mutil.thy	Thu May 31 18:28:23 2001 +0200
@@ -8,7 +8,7 @@
   Popularized as the Mutilated Checkerboard Problem by J McCarthy
 *)
 
-Mutil = CardinalArith +
+Mutil = Main +
 consts
   domino  :: i
   tiling  :: i=>i
diff -r 7f6eff7bc97a -r 9b80fe19407f src/ZF/ex/Ntree.thy
--- a/src/ZF/ex/Ntree.thy	Thu May 31 17:57:02 2001 +0200
+++ b/src/ZF/ex/Ntree.thy	Thu May 31 18:28:23 2001 +0200
@@ -9,7 +9,7 @@
 Based upon ex/Term.thy
 *)
 
-Ntree = InfDatatype +
+Ntree = Main +
 consts
   ntree    :: i=>i
   maptree  :: i=>i
diff -r 7f6eff7bc97a -r 9b80fe19407f src/ZF/ex/PropLog.thy
--- a/src/ZF/ex/PropLog.thy	Thu May 31 17:57:02 2001 +0200
+++ b/src/ZF/ex/PropLog.thy	Thu May 31 18:28:23 2001 +0200
@@ -7,7 +7,7 @@
 of the propositional tautologies.
 *)
 
-PropLog = Finite + Datatype +
+PropLog = Main +
 
 (** The datatype of propositions; note mixfix syntax **)
 consts
diff -r 7f6eff7bc97a -r 9b80fe19407f src/ZF/ex/Ramsey.thy
--- a/src/ZF/ex/Ramsey.thy	Thu May 31 17:57:02 2001 +0200
+++ b/src/ZF/ex/Ramsey.thy	Thu May 31 18:28:23 2001 +0200
@@ -18,7 +18,7 @@
     Available from the author: kaufmann@cli.com
 *)
 
-Ramsey = Arith +
+Ramsey = Main +
 consts
   Symmetric             :: i=>o
   Atleast               :: [i,i]=>o
diff -r 7f6eff7bc97a -r 9b80fe19407f src/ZF/ex/Rmap.thy
--- a/src/ZF/ex/Rmap.thy	Thu May 31 17:57:02 2001 +0200
+++ b/src/ZF/ex/Rmap.thy	Thu May 31 18:28:23 2001 +0200
@@ -6,7 +6,7 @@
 Inductive definition of an operator to "map" a relation over a list
 *)
 
-Rmap = List +
+Rmap = Main +
 
 consts
   rmap :: i=>i
diff -r 7f6eff7bc97a -r 9b80fe19407f src/ZF/ex/TF.thy
--- a/src/ZF/ex/TF.thy	Thu May 31 17:57:02 2001 +0200
+++ b/src/ZF/ex/TF.thy	Thu May 31 18:28:23 2001 +0200
@@ -6,7 +6,7 @@
 Trees & forests, a mutually recursive type definition.
 *)
 
-TF = List +
+TF = Main +
 consts
   tree, forest, tree_forest    :: i=>i
 
diff -r 7f6eff7bc97a -r 9b80fe19407f src/ZF/ex/Term.thy
--- a/src/ZF/ex/Term.thy	Thu May 31 17:57:02 2001 +0200
+++ b/src/ZF/ex/Term.thy	Thu May 31 18:28:23 2001 +0200
@@ -7,7 +7,7 @@
 Illustrates the list functor (essentially the same type as in Trees & Forests)
 *)
 
-Term = List +
+Term = Main +
 consts
   term      :: i=>i