--- a/src/ZF/Datatype.ML Thu Apr 26 15:41:49 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,105 +0,0 @@
-(* Title: ZF/Datatype.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-
-(Co)Datatype Definitions for Zermelo-Fraenkel Set Theory
-*)
-
-
-(*Typechecking rules for most datatypes involving univ*)
-structure Data_Arg =
- struct
- val intrs =
- [SigmaI, InlI, InrI,
- Pair_in_univ, Inl_in_univ, Inr_in_univ,
- zero_in_univ, A_into_univ, nat_into_univ, UnCI];
-
-
- val elims = [make_elim InlD, make_elim InrD, (*for mutual recursion*)
- SigmaE, sumE]; (*allows * and + in spec*)
- end;
-
-
-structure Data_Package =
- Add_datatype_def_Fun
- (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
- and Su=Standard_Sum
- and Ind_Package = Ind_Package
- and Datatype_Arg = Data_Arg
- val coind = false);
-
-
-(*Typechecking rules for most codatatypes involving quniv*)
-structure CoData_Arg =
- struct
- val intrs =
- [QSigmaI, QInlI, QInrI,
- QPair_in_quniv, QInl_in_quniv, QInr_in_quniv,
- zero_in_quniv, A_into_quniv, nat_into_quniv, UnCI];
-
- val elims = [make_elim QInlD, make_elim QInrD, (*for mutual recursion*)
- QSigmaE, qsumE]; (*allows * and + in spec*)
- end;
-
-structure CoData_Package =
- Add_datatype_def_Fun
- (structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
- and Su=Quine_Sum
- and Ind_Package = CoInd_Package
- and Datatype_Arg = CoData_Arg
- val coind = true);
-
-
-
-(*Simproc for freeness reasoning: compare datatype constructors for equality*)
-structure DataFree =
-struct
- val trace = ref false;
-
- fun mk_new ([],[]) = Const("True",FOLogic.oT)
- | mk_new (largs,rargs) =
- fold_bal FOLogic.mk_conj
- (map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
-
- val datatype_ss = simpset ();
-
- fun proc sg ss old =
- let val _ = if !trace then writeln ("data_free: OLD = " ^
- string_of_cterm (cterm_of sg old))
- else ()
- val (lhs,rhs) = FOLogic.dest_eq old
- val (lhead, largs) = strip_comb lhs
- and (rhead, rargs) = strip_comb rhs
- val lname = #1 (dest_Const lhead) handle TERM _ => raise Match;
- val rname = #1 (dest_Const rhead) handle TERM _ => raise Match;
- val lcon_info = the (Symtab.lookup (ConstructorsData.get sg) lname)
- handle Option => raise Match;
- val rcon_info = the (Symtab.lookup (ConstructorsData.get sg) rname)
- handle Option => raise Match;
- val new =
- if #big_rec_name lcon_info = #big_rec_name rcon_info
- andalso not (null (#free_iffs lcon_info)) then
- if lname = rname then mk_new (largs, rargs)
- else Const("False",FOLogic.oT)
- else raise Match
- val _ = if !trace then
- writeln ("NEW = " ^ string_of_cterm (Thm.cterm_of sg new))
- else ();
- val goal = Logic.mk_equals (old, new)
- val thm = Goal.prove (Simplifier.the_context ss) [] [] goal
- (fn _ => rtac iff_reflection 1 THEN
- simp_tac (Simplifier.inherit_context ss datatype_ss addsimps #free_iffs lcon_info) 1)
- handle ERROR msg =>
- (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Sign.string_of_term sg goal);
- raise Match)
- in SOME thm end
- handle Match => NONE;
-
-
- val conv = Simplifier.simproc (theory "ZF") "data_free" ["(x::i) = y"] proc;
-
-end;
-
-
-Addsimprocs [DataFree.conv];
--- a/src/ZF/Datatype.thy Thu Apr 26 15:41:49 2007 +0200
+++ b/src/ZF/Datatype.thy Thu Apr 26 15:42:04 2007 +0200
@@ -7,9 +7,108 @@
header{*Datatype and CoDatatype Definitions*}
-theory Datatype imports Inductive Univ QUniv
- uses
- "Tools/datatype_package.ML"
- "Tools/numeral_syntax.ML" begin (*belongs to theory Bin*)
+theory Datatype
+imports Inductive Univ QUniv
+uses "Tools/datatype_package.ML"
+begin
+
+ML_setup {*
+(*Typechecking rules for most datatypes involving univ*)
+structure Data_Arg =
+ struct
+ val intrs =
+ [SigmaI, InlI, InrI,
+ Pair_in_univ, Inl_in_univ, Inr_in_univ,
+ zero_in_univ, A_into_univ, nat_into_univ, UnCI];
+
+
+ val elims = [make_elim InlD, make_elim InrD, (*for mutual recursion*)
+ SigmaE, sumE]; (*allows * and + in spec*)
+ end;
+
+
+structure Data_Package =
+ Add_datatype_def_Fun
+ (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
+ and Su=Standard_Sum
+ and Ind_Package = Ind_Package
+ and Datatype_Arg = Data_Arg
+ val coind = false);
+
+
+(*Typechecking rules for most codatatypes involving quniv*)
+structure CoData_Arg =
+ struct
+ val intrs =
+ [QSigmaI, QInlI, QInrI,
+ QPair_in_quniv, QInl_in_quniv, QInr_in_quniv,
+ zero_in_quniv, A_into_quniv, nat_into_quniv, UnCI];
+
+ val elims = [make_elim QInlD, make_elim QInrD, (*for mutual recursion*)
+ QSigmaE, qsumE]; (*allows * and + in spec*)
+ end;
+
+structure CoData_Package =
+ Add_datatype_def_Fun
+ (structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
+ and Su=Quine_Sum
+ and Ind_Package = CoInd_Package
+ and Datatype_Arg = CoData_Arg
+ val coind = true);
+
+
+
+(*Simproc for freeness reasoning: compare datatype constructors for equality*)
+structure DataFree =
+struct
+ val trace = ref false;
+
+ fun mk_new ([],[]) = Const("True",FOLogic.oT)
+ | mk_new (largs,rargs) =
+ fold_bal FOLogic.mk_conj
+ (map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
+
+ val datatype_ss = @{simpset};
+
+ fun proc sg ss old =
+ let val _ = if !trace then writeln ("data_free: OLD = " ^
+ string_of_cterm (cterm_of sg old))
+ else ()
+ val (lhs,rhs) = FOLogic.dest_eq old
+ val (lhead, largs) = strip_comb lhs
+ and (rhead, rargs) = strip_comb rhs
+ val lname = #1 (dest_Const lhead) handle TERM _ => raise Match;
+ val rname = #1 (dest_Const rhead) handle TERM _ => raise Match;
+ val lcon_info = the (Symtab.lookup (ConstructorsData.get sg) lname)
+ handle Option => raise Match;
+ val rcon_info = the (Symtab.lookup (ConstructorsData.get sg) rname)
+ handle Option => raise Match;
+ val new =
+ if #big_rec_name lcon_info = #big_rec_name rcon_info
+ andalso not (null (#free_iffs lcon_info)) then
+ if lname = rname then mk_new (largs, rargs)
+ else Const("False",FOLogic.oT)
+ else raise Match
+ val _ = if !trace then
+ writeln ("NEW = " ^ string_of_cterm (Thm.cterm_of sg new))
+ else ();
+ val goal = Logic.mk_equals (old, new)
+ val thm = Goal.prove (Simplifier.the_context ss) [] [] goal
+ (fn _ => rtac iff_reflection 1 THEN
+ simp_tac (Simplifier.inherit_context ss datatype_ss addsimps #free_iffs lcon_info) 1)
+ handle ERROR msg =>
+ (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Sign.string_of_term sg goal);
+ raise Match)
+ in SOME thm end
+ handle Match => NONE;
+
+
+ val conv = Simplifier.simproc @{theory} "data_free" ["(x::i) = y"] proc;
+
+end;
+
+
+Addsimprocs [DataFree.conv];
+*}
end
--- a/src/ZF/Inductive.ML Thu Apr 26 15:41:49 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,108 +0,0 @@
-(* Title: ZF/Inductive.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-
-(Co)Inductive Definitions for Zermelo-Fraenkel Set Theory
-
-Inductive definitions use least fixedpoints with standard products and sums
-Coinductive definitions use greatest fixedpoints with Quine products and sums
-
-Sums are used only for mutual recursion;
-Products are used only to derive "streamlined" induction rules for relations
-*)
-
-val iT = Ind_Syntax.iT
-and oT = FOLogic.oT;
-
-structure Lfp =
- struct
- val oper = Const("Fixedpt.lfp", [iT,iT-->iT]--->iT)
- val bnd_mono = Const("Fixedpt.bnd_mono", [iT,iT-->iT]--->oT)
- val bnd_monoI = bnd_monoI
- val subs = def_lfp_subset
- val Tarski = def_lfp_unfold
- val induct = def_induct
- end;
-
-structure Standard_Prod =
- struct
- val sigma = Const("Sigma", [iT, iT-->iT]--->iT)
- val pair = Const("Pair", [iT,iT]--->iT)
- val split_name = "split"
- val pair_iff = Pair_iff
- val split_eq = split
- val fsplitI = splitI
- val fsplitD = splitD
- val fsplitE = splitE
- end;
-
-structure Standard_CP = CartProd_Fun (Standard_Prod);
-
-structure Standard_Sum =
- struct
- val sum = Const("op +", [iT,iT]--->iT)
- val inl = Const("Inl", iT-->iT)
- val inr = Const("Inr", iT-->iT)
- val elim = Const("case", [iT-->iT, iT-->iT, iT]--->iT)
- val case_inl = case_Inl
- val case_inr = case_Inr
- val inl_iff = Inl_iff
- val inr_iff = Inr_iff
- val distinct = Inl_Inr_iff
- val distinct' = Inr_Inl_iff
- val free_SEs = Ind_Syntax.mk_free_SEs
- [distinct, distinct', inl_iff, inr_iff, Standard_Prod.pair_iff]
- end;
-
-
-structure Ind_Package =
- Add_inductive_def_Fun
- (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
- and Su=Standard_Sum val coind = false);
-
-
-structure Gfp =
- struct
- val oper = Const("Fixedpt.gfp", [iT,iT-->iT]--->iT)
- val bnd_mono = Const("Fixedpt.bnd_mono", [iT,iT-->iT]--->oT)
- val bnd_monoI = bnd_monoI
- val subs = def_gfp_subset
- val Tarski = def_gfp_unfold
- val induct = def_Collect_coinduct
- end;
-
-structure Quine_Prod =
- struct
- val sigma = Const("QPair.QSigma", [iT, iT-->iT]--->iT)
- val pair = Const("QPair.QPair", [iT,iT]--->iT)
- val split_name = "QPair.qsplit"
- val pair_iff = QPair_iff
- val split_eq = qsplit
- val fsplitI = qsplitI
- val fsplitD = qsplitD
- val fsplitE = qsplitE
- end;
-
-structure Quine_CP = CartProd_Fun (Quine_Prod);
-
-structure Quine_Sum =
- struct
- val sum = Const("QPair.op <+>", [iT,iT]--->iT)
- val inl = Const("QPair.QInl", iT-->iT)
- val inr = Const("QPair.QInr", iT-->iT)
- val elim = Const("QPair.qcase", [iT-->iT, iT-->iT, iT]--->iT)
- val case_inl = qcase_QInl
- val case_inr = qcase_QInr
- val inl_iff = QInl_iff
- val inr_iff = QInr_iff
- val distinct = QInl_QInr_iff
- val distinct' = QInr_QInl_iff
- val free_SEs = Ind_Syntax.mk_free_SEs
- [distinct, distinct', inl_iff, inr_iff, Quine_Prod.pair_iff]
- end;
-
-
-structure CoInd_Package =
- Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
- and Su=Quine_Sum val coind = true);
--- a/src/ZF/Inductive.thy Thu Apr 26 15:41:49 2007 +0200
+++ b/src/ZF/Inductive.thy Thu Apr 26 15:42:04 2007 +0200
@@ -3,6 +3,11 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
+Inductive definitions use least fixedpoints with standard products and sums
+Coinductive definitions use greatest fixedpoints with Quine products and sums
+
+Sums are used only for mutual recursion;
+Products are used only to derive "streamlined" induction rules for relations
*)
header{*Inductive and Coinductive Definitions*}
@@ -19,4 +24,102 @@
setup IndCases.setup
setup DatatypeTactics.setup
+ML_setup {*
+val iT = Ind_Syntax.iT
+and oT = FOLogic.oT;
+
+structure Lfp =
+ struct
+ val oper = Const("Fixedpt.lfp", [iT,iT-->iT]--->iT)
+ val bnd_mono = Const("Fixedpt.bnd_mono", [iT,iT-->iT]--->oT)
+ val bnd_monoI = bnd_monoI
+ val subs = def_lfp_subset
+ val Tarski = def_lfp_unfold
+ val induct = def_induct
+ end;
+
+structure Standard_Prod =
+ struct
+ val sigma = Const("Sigma", [iT, iT-->iT]--->iT)
+ val pair = Const("Pair", [iT,iT]--->iT)
+ val split_name = "split"
+ val pair_iff = Pair_iff
+ val split_eq = split
+ val fsplitI = splitI
+ val fsplitD = splitD
+ val fsplitE = splitE
+ end;
+
+structure Standard_CP = CartProd_Fun (Standard_Prod);
+
+structure Standard_Sum =
+ struct
+ val sum = Const("op +", [iT,iT]--->iT)
+ val inl = Const("Inl", iT-->iT)
+ val inr = Const("Inr", iT-->iT)
+ val elim = Const("case", [iT-->iT, iT-->iT, iT]--->iT)
+ val case_inl = case_Inl
+ val case_inr = case_Inr
+ val inl_iff = Inl_iff
+ val inr_iff = Inr_iff
+ val distinct = Inl_Inr_iff
+ val distinct' = Inr_Inl_iff
+ val free_SEs = Ind_Syntax.mk_free_SEs
+ [distinct, distinct', inl_iff, inr_iff, Standard_Prod.pair_iff]
+ end;
+
+
+structure Ind_Package =
+ Add_inductive_def_Fun
+ (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
+ and Su=Standard_Sum val coind = false);
+
+
+structure Gfp =
+ struct
+ val oper = Const("Fixedpt.gfp", [iT,iT-->iT]--->iT)
+ val bnd_mono = Const("Fixedpt.bnd_mono", [iT,iT-->iT]--->oT)
+ val bnd_monoI = bnd_monoI
+ val subs = def_gfp_subset
+ val Tarski = def_gfp_unfold
+ val induct = def_Collect_coinduct
+ end;
+
+structure Quine_Prod =
+ struct
+ val sigma = Const("QPair.QSigma", [iT, iT-->iT]--->iT)
+ val pair = Const("QPair.QPair", [iT,iT]--->iT)
+ val split_name = "QPair.qsplit"
+ val pair_iff = QPair_iff
+ val split_eq = qsplit
+ val fsplitI = qsplitI
+ val fsplitD = qsplitD
+ val fsplitE = qsplitE
+ end;
+
+structure Quine_CP = CartProd_Fun (Quine_Prod);
+
+structure Quine_Sum =
+ struct
+ val sum = Const("QPair.op <+>", [iT,iT]--->iT)
+ val inl = Const("QPair.QInl", iT-->iT)
+ val inr = Const("QPair.QInr", iT-->iT)
+ val elim = Const("QPair.qcase", [iT-->iT, iT-->iT, iT]--->iT)
+ val case_inl = qcase_QInl
+ val case_inr = qcase_QInr
+ val inl_iff = QInl_iff
+ val inr_iff = QInr_iff
+ val distinct = QInl_QInr_iff
+ val distinct' = QInr_QInl_iff
+ val free_SEs = Ind_Syntax.mk_free_SEs
+ [distinct, distinct', inl_iff, inr_iff, Quine_Prod.pair_iff]
+ end;
+
+
+structure CoInd_Package =
+ Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
+ and Su=Quine_Sum val coind = true);
+
+*}
+
end
--- a/src/ZF/Integ/Bin.thy Thu Apr 26 15:41:49 2007 +0200
+++ b/src/ZF/Integ/Bin.thy Thu Apr 26 15:42:04 2007 +0200
@@ -16,7 +16,10 @@
header{*Arithmetic on Binary Integers*}
-theory Bin imports Int Datatype begin
+theory Bin
+imports Int Datatype
+uses "Tools/numeral_syntax.ML"
+begin
consts bin :: i
datatype
--- a/src/ZF/IsaMakefile Thu Apr 26 15:41:49 2007 +0200
+++ b/src/ZF/IsaMakefile Thu Apr 26 15:42:04 2007 +0200
@@ -28,24 +28,18 @@
FOL:
@cd $(SRC)/FOL; $(ISATOOL) make FOL
-$(OUT)/ZF$(ML_SUFFIX): $(OUT)/FOL$(ML_SUFFIX) AC.thy Arith.thy \
- ArithSimp.thy Bool.thy Cardinal.thy \
- CardinalArith.thy Cardinal_AC.thy \
- Datatype.ML Datatype.thy Epsilon.thy Finite.thy \
- Fixedpt.thy Inductive.ML Inductive.thy \
- InfDatatype.thy Integ/Bin.thy \
- Integ/EquivClass.thy Integ/Int.thy Integ/IntArith.thy \
- Integ/IntDiv.thy Integ/int_arith.ML \
- List.thy Main.ML Main.thy \
- Main_ZFC.ML Main_ZFC.thy Nat.thy Order.thy OrderArith.thy \
- OrderType.thy Ordinal.thy OrdQuant.thy Perm.thy \
- QPair.thy QUniv.thy ROOT.ML \
- Sum.thy Tools/cartprod.ML Tools/datatype_package.ML \
- Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML \
- Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML \
- Trancl.thy Univ.thy \
- WF.thy ZF.thy Zorn.thy arith_data.ML equalities.thy func.thy \
- ind_syntax.ML pair.thy simpdata.ML upair.thy
+$(OUT)/ZF$(ML_SUFFIX): $(OUT)/FOL$(ML_SUFFIX) AC.thy Arith.thy \
+ ArithSimp.thy Bool.thy Cardinal.thy CardinalArith.thy Cardinal_AC.thy \
+ Datatype.thy Epsilon.thy Finite.thy Fixedpt.thy Inductive.thy \
+ InfDatatype.thy Integ/Bin.thy Integ/EquivClass.thy Integ/Int.thy \
+ Integ/IntArith.thy Integ/IntDiv.thy Integ/int_arith.ML List.thy \
+ Main.thy Main_ZFC.thy Nat.thy OrdQuant.thy Order.thy OrderArith.thy \
+ OrderType.thy Ordinal.thy Perm.thy QPair.thy QUniv.thy ROOT.ML Sum.thy \
+ Tools/cartprod.ML Tools/datatype_package.ML Tools/ind_cases.ML \
+ Tools/induct_tacs.ML Tools/inductive_package.ML \
+ Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML \
+ Trancl.thy Univ.thy WF.thy ZF.thy Zorn.thy arith_data.ML \
+ equalities.thy func.thy ind_syntax.ML pair.thy simpdata.ML upair.thy
@$(ISATOOL) usedir -b -r $(OUT)/FOL ZF
--- a/src/ZF/Main.ML Thu Apr 26 15:41:49 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-
-(* $Id$ *)
-
-structure Main =
-struct
- val thy = the_context ();
-end;
--- a/src/ZF/Main.thy Thu Apr 26 15:41:49 2007 +0200
+++ b/src/ZF/Main.thy Thu Apr 26 15:42:04 2007 +0200
@@ -5,8 +5,8 @@
theory Main imports List IntDiv CardinalArith begin
(*The theory of "iterates" logically belongs to Nat, but can't go there because
- primrec isn't available into after Datatype. The only theories defined
- after Datatype are List and the Integ theories.*)
+ primrec isn't available into after Datatype.*)
+
subsection{* Iteration of the function @{term F} *}
consts iterates :: "[i=>i,i,i] => i" ("(_^_ '(_'))" [60,1000,1000] 60)
--- a/src/ZF/Main_ZFC.ML Thu Apr 26 15:41:49 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,92 +0,0 @@
-structure Main_ZFC =
-struct
- val thy = the_context ();
-end;
-
-(* legacy ML bindings *)
-
-(* from AC *)
-val AC_Pi = thm "AC_Pi";
-val AC_ball_Pi = thm "AC_ball_Pi";
-val AC_Pi_Pow = thm "AC_Pi_Pow";
-val AC_func = thm "AC_func";
-val non_empty_family = thm "non_empty_family";
-val AC_func0 = thm "AC_func0";
-val AC_func_Pow = thm "AC_func_Pow";
-val AC_Pi0 = thm "AC_Pi0";
-val choice_Diff = thm "choice_Diff";
-
-(* from Zorn *)
-val Union_lemma0 = thm "Union_lemma0";
-val Inter_lemma0 = thm "Inter_lemma0";
-val increasingD1 = thm "increasingD1";
-val increasingD2 = thm "increasingD2";
-val TFin_UnionI = thm "TFin_UnionI";
-val TFin_is_subset = thm "TFin_is_subset";
-val TFin_induct = thm "TFin_induct";
-val increasing_trans = thm "increasing_trans";
-val TFin_linear_lemma1 = thm "TFin_linear_lemma1";
-val TFin_linear_lemma2 = thm "TFin_linear_lemma2";
-val TFin_subsetD = thm "TFin_subsetD";
-val TFin_subset_linear = thm "TFin_subset_linear";
-val equal_next_upper = thm "equal_next_upper";
-val equal_next_Union = thm "equal_next_Union";
-val chain_subset_Pow = thm "chain_subset_Pow";
-val super_subset_chain = thm "super_subset_chain";
-val maxchain_subset_chain = thm "maxchain_subset_chain";
-val choice_super = thm "choice_super";
-val choice_not_equals = thm "choice_not_equals";
-val Hausdorff_next_exists = thm "Hausdorff_next_exists";
-val TFin_chain_lemma4 = thm "TFin_chain_lemma4";
-val Hausdorff = thm "Hausdorff";
-val chain_extend = thm "chain_extend";
-val Zorn = thm "Zorn";
-val TFin_well_lemma5 = thm "TFin_well_lemma5";
-val well_ord_TFin_lemma = thm "well_ord_TFin_lemma";
-val well_ord_TFin = thm "well_ord_TFin";
-val Zermelo_next_exists = thm "Zermelo_next_exists";
-val choice_imp_injection = thm "choice_imp_injection";
-val AC_well_ord = thm "AC_well_ord";
-
-(* from Cardinal_AC *)
-val cardinal_eqpoll = thm "cardinal_eqpoll";
-val cardinal_idem = thm "cardinal_idem";
-val cardinal_eqE = thm "cardinal_eqE";
-val cardinal_eqpoll_iff = thm "cardinal_eqpoll_iff";
-val cardinal_disjoint_Un = thm "cardinal_disjoint_Un";
-val lepoll_imp_Card_le = thm "lepoll_imp_Card_le";
-val cadd_assoc = thm "cadd_assoc";
-val cmult_assoc = thm "cmult_assoc";
-val cadd_cmult_distrib = thm "cadd_cmult_distrib";
-val InfCard_square_eq = thm "InfCard_square_eq";
-val Card_le_imp_lepoll = thm "Card_le_imp_lepoll";
-val le_Card_iff = thm "le_Card_iff";
-val surj_implies_inj = thm "surj_implies_inj";
-val surj_implies_cardinal_le = thm "surj_implies_cardinal_le";
-val cardinal_UN_le = thm "cardinal_UN_le";
-val cardinal_UN_lt_csucc = thm "cardinal_UN_lt_csucc";
-val cardinal_UN_Ord_lt_csucc = thm "cardinal_UN_Ord_lt_csucc";
-val inj_UN_subset = thm "inj_UN_subset";
-val le_UN_Ord_lt_csucc = thm "le_UN_Ord_lt_csucc";
-
-(* from InfDatatype *)
-val fun_Limit_VfromE = thm "fun_Limit_VfromE";
-val fun_Vcsucc_lemma = thm "fun_Vcsucc_lemma";
-val subset_Vcsucc = thm "subset_Vcsucc";
-val fun_Vcsucc = thm "fun_Vcsucc";
-val fun_in_Vcsucc = thm "fun_in_Vcsucc";
-val fun_in_Vcsucc' = thm "fun_in_Vcsucc'";
-val Card_fun_Vcsucc = thm "Card_fun_Vcsucc";
-val Card_fun_in_Vcsucc = thm "Card_fun_in_Vcsucc";
-val Limit_csucc = thm "Limit_csucc";
-val Pair_in_Vcsucc = thm "Pair_in_Vcsucc";
-val Inl_in_Vcsucc = thm "Inl_in_Vcsucc";
-val Inr_in_Vcsucc = thm "Inr_in_Vcsucc";
-val zero_in_Vcsucc = thm "zero_in_Vcsucc";
-val nat_into_Vcsucc = thm "nat_into_Vcsucc";
-val InfCard_nat_Un_cardinal = thm "InfCard_nat_Un_cardinal";
-val le_nat_Un_cardinal = thm "le_nat_Un_cardinal";
-val UN_upper_cardinal = thm "UN_upper_cardinal";
-
-val inf_datatype_intrs = thms "inf_datatype_intros";
-