--- 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"
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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