--- a/src/ZF/Fixedpt.thy Tue Jan 12 13:54:51 1999 +0100
+++ b/src/ZF/Fixedpt.thy Tue Jan 12 15:17:37 1999 +0100
@@ -8,14 +8,10 @@
Fixedpt = domrange +
-global
-
consts
bnd_mono :: [i,i=>i]=>o
lfp, gfp :: [i,i=>i]=>i
-local
-
defs
(*monotone operator from Pow(D) to itself*)
bnd_mono_def
--- a/src/ZF/Inductive.ML Tue Jan 12 13:54:51 1999 +0100
+++ b/src/ZF/Inductive.ML Tue Jan 12 15:17:37 1999 +0100
@@ -17,8 +17,8 @@
structure Lfp =
struct
- val oper = Const("lfp", [iT,iT-->iT]--->iT)
- val bnd_mono = Const("bnd_mono", [iT,iT-->iT]--->oT)
+ 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_Tarski
@@ -64,8 +64,8 @@
structure Gfp =
struct
- val oper = Const("gfp", [iT,iT-->iT]--->iT)
- val bnd_mono = Const("bnd_mono", [iT,iT-->iT]--->oT)
+ 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_Tarski
@@ -74,9 +74,9 @@
structure Quine_Prod =
struct
- val sigma = Const("QSigma", [iT, iT-->iT]--->iT)
- val pair = Const("QPair", [iT,iT]--->iT)
- val split_name = "qsplit"
+ 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
@@ -88,10 +88,10 @@
structure Quine_Sum =
struct
- val sum = Const("op <+>", [iT,iT]--->iT)
- val inl = Const("QInl", iT-->iT)
- val inr = Const("QInr", iT-->iT)
- val elim = Const("qcase", [iT-->iT, iT-->iT, iT]--->iT)
+ 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
--- a/src/ZF/OrdQuant.ML Tue Jan 12 13:54:51 1999 +0100
+++ b/src/ZF/OrdQuant.ML Tue Jan 12 15:17:37 1999 +0100
@@ -95,7 +95,7 @@
AddSEs [oexE, OUN_E];
AddEs [rev_oallE];
-val Ord_atomize = atomize (("oall", [ospec])::ZF_conn_pairs,
+val Ord_atomize = atomize (("OrdQuant.oall", [ospec])::ZF_conn_pairs,
ZF_mem_pairs);
simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all)
--- a/src/ZF/OrdQuant.thy Tue Jan 12 13:54:51 1999 +0100
+++ b/src/ZF/OrdQuant.thy Tue Jan 12 15:17:37 1999 +0100
@@ -7,8 +7,6 @@
OrdQuant = Ordinal +
-global
-
consts
(* Ordinal Quantifiers *)
@@ -32,8 +30,6 @@
"@oex" :: [idt, i, o] => o ("(3\\<exists> _<_./ _)" 10)
"@OUNION" :: [idt, i, i] => i ("(3\\<Union> _<_./ _)" 10)
-local
-
defs
(* Ordinal Quantifiers *)
--- a/src/ZF/QPair.thy Tue Jan 12 13:54:51 1999 +0100
+++ b/src/ZF/QPair.thy Tue Jan 12 15:17:37 1999 +0100
@@ -13,8 +13,6 @@
QPair = Sum +
-global
-
consts
QPair :: [i, i] => i ("<(_;/ _)>")
qfst,qsnd :: i => i
@@ -34,7 +32,6 @@
"QSUM x:A. B" => "QSigma(A, %x. B)"
"A <*> B" => "QSigma(A, _K(B))"
-local
defs
QPair_def "<a;b> == a+b"
--- a/src/ZF/QUniv.thy Tue Jan 12 13:54:51 1999 +0100
+++ b/src/ZF/QUniv.thy Tue Jan 12 15:17:37 1999 +0100
@@ -1,21 +1,15 @@
-(* Title: ZF/univ.thy
+(* Title: ZF/QUniv.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-A small universe for lazy recursive types
+A small universe for lazy recursive types.
*)
QUniv = Univ + QPair + mono + equalities +
-global
-
-consts
- quniv :: i=>i
-
-local
-
-defs
- quniv_def "quniv(A) == Pow(univ(eclose(A)))"
+constdefs
+ quniv :: i => i
+ "quniv(A) == Pow(univ(eclose(A)))"
end
--- a/src/ZF/Tools/datatype_package.ML Tue Jan 12 13:54:51 1999 +0100
+++ b/src/ZF/Tools/datatype_package.ML Tue Jan 12 15:17:37 1999 +0100
@@ -80,7 +80,7 @@
val intr_tms = Ind_Syntax.mk_all_intr_tms sign (rec_tms, con_ty_lists)
val dummy =
- writeln ((if (#1 (dest_Const Fp.oper) = "lfp") then "Datatype"
+ writeln ((if (#1 (dest_Const Fp.oper) = "Fixedpt.lfp") then "Datatype"
else "Codatatype")
^ " definition " ^ big_rec_name)
@@ -239,7 +239,7 @@
(* Build the new theory *)
val need_recursor =
- (#1 (dest_Const Fp.oper) = "lfp" andalso recursor_typ <> case_typ);
+ (#1 (dest_Const Fp.oper) = "Fixedpt.lfp" andalso recursor_typ <> case_typ);
fun add_recursor thy =
if need_recursor then
@@ -415,7 +415,7 @@
val rec_tms = map (readtm sign Ind_Syntax.iT) srec_tms
val dom_sum =
if sdom = "" then
- Ind_Syntax.data_domain (#1 (dest_Const Fp.oper) <> "lfp") rec_tms
+ Ind_Syntax.data_domain (#1 (dest_Const Fp.oper) <> "Fixedpt.lfp") rec_tms
else readtm sign Ind_Syntax.iT sdom
and con_ty_lists = Ind_Syntax.read_constructs sign scon_ty_lists
in
--- a/src/ZF/Tools/inductive_package.ML Tue Jan 12 13:54:51 1999 +0100
+++ b/src/ZF/Tools/inductive_package.ML Tue Jan 12 15:17:37 1999 +0100
@@ -141,7 +141,7 @@
val dummy =
if verbose then
- writeln ((if #1 (dest_Const Fp.oper) = "lfp" then "Inductive"
+ writeln ((if #1 (dest_Const Fp.oper) = "Fixedpt.lfp" then "Inductive"
else "Coinductive") ^ " definition " ^ big_rec_name)
else ();
@@ -528,7 +528,7 @@
val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct)
val (thy2, induct, mutual_induct) =
- if #1 (dest_Const Fp.oper) = "lfp" then induction_rules raw_induct thy1
+ if #1 (dest_Const Fp.oper) = "Fixedpt.lfp" then induction_rules raw_induct thy1
else (thy1, raw_induct, TrueI)
and defs = big_rec_def :: part_rec_defs
--- a/src/ZF/Univ.thy Tue Jan 12 13:54:51 1999 +0100
+++ b/src/ZF/Univ.thy Tue Jan 12 15:17:37 1999 +0100
@@ -8,13 +8,11 @@
Standard notation for Vset(i) is V(i), but users might want V for a variable
NOTE: univ(A) could be a translation; would simplify many proofs!
- But Ind_Syntax.univ refers to the constant "univ"
+ But Ind_Syntax.univ refers to the constant "Univ.univ"
*)
Univ = Arith + Sum + Finite + mono +
-global
-
consts
Vfrom :: [i,i]=>i
Vset :: i=>i
@@ -25,7 +23,6 @@
translations
"Vset(x)" == "Vfrom(0,x)"
-local
defs
Vfrom_def "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))"
--- a/src/ZF/ind_syntax.ML Tue Jan 12 13:54:51 1999 +0100
+++ b/src/ZF/ind_syntax.ML Tue Jan 12 15:17:37 1999 +0100
@@ -35,7 +35,7 @@
val apply_const = Const("op `", [iT,iT]--->iT);
-val Vrecursor_const = Const("Vrecursor", [[iT,iT]--->iT, iT]--->iT);
+val Vrecursor_const = Const("Univ.Vrecursor", [[iT,iT]--->iT, iT]--->iT);
val Collect_const = Const("Collect", [iT, iT-->FOLogic.oT] ---> iT);
fun mk_Collect (a,D,t) = Collect_const $ D $ absfree(a, iT, t);
@@ -103,8 +103,8 @@
val Un = Const("op Un", [iT,iT]--->iT)
and empty = Const("0", iT)
-and univ = Const("univ", iT-->iT)
-and quniv = Const("quniv", iT-->iT);
+and univ = Const("Univ.univ", iT-->iT)
+and quniv = Const("QUniv.quniv", iT-->iT);
(*Make a datatype's domain: form the union of its set parameters*)
fun union_params rec_tm =
--- a/src/ZF/thy_syntax.ML Tue Jan 12 13:54:51 1999 +0100
+++ b/src/ZF/thy_syntax.ML Tue Jan 12 15:17:37 1999 +0100
@@ -14,7 +14,7 @@
(*ML identifiers for introduction rules.*)
fun mk_intr_name suffix s =
- if Syntax.is_identifier s then
+ if ThmDatabase.is_ml_identifier s then
"op " ^ s ^ suffix (*the "op" cancels any infix status*)
else "_"; (*bad name, don't try to bind*)