--- a/src/ZF/Coind/ECR.thy Wed Jan 13 12:44:33 1999 +0100
+++ b/src/ZF/Coind/ECR.thy Wed Jan 13 15:14:47 1999 +0100
@@ -22,7 +22,7 @@
{<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}:Pow(HasTyRel)
|] ==>
<v_clos(x,e,ve),t>:HasTyRel"
- monos "[Pow_mono]"
+ monos Pow_mono
type_intrs "Val_ValEnv.intrs"
(* Pointwise extension to environments *)
--- a/src/ZF/Coind/Values.thy Wed Jan 13 12:44:33 1999 +0100
+++ b/src/ZF/Coind/Values.thy Wed Jan 13 15:14:47 1999 +0100
@@ -16,8 +16,8 @@
| v_clos ("x:ExVar","e:Exp","ve:ValEnv")
and
"ValEnv" = ve_mk ("m:PMap(ExVar,Val)")
- monos "[map_mono]"
- type_intrs "[A_into_univ, mapQU]"
+ monos map_mono
+ type_intrs A_into_univ, mapQU
consts
ve_owr :: [i,i,i] => i
--- a/src/ZF/Integ/Bin.thy Wed Jan 13 12:44:33 1999 +0100
+++ b/src/ZF/Integ/Bin.thy Wed Jan 13 15:14:47 1999 +0100
@@ -20,6 +20,15 @@
Bin = Int + Datatype +
+consts bin :: i
+datatype
+ "bin" = Pls
+ | Min
+ | Cons ("w: bin", "b: bool")
+
+syntax
+ "_Int" :: xnum => i ("_")
+
consts
integ_of :: i=>i
NCons :: [i,i]=>i
@@ -30,18 +39,6 @@
adding :: [i,i,i]=>i
bin_mult :: [i,i]=>i
- bin :: i
-
-syntax
- "_Int" :: xnum => i ("_")
-
-datatype
- "bin" = Pls
- | Min
- | Cons ("w: bin", "b: bool")
- type_intrs "[bool_into_univ]"
-
-
primrec
"integ_of (Pls) = $# 0"
"integ_of (Min) = $~($#1)"
--- a/src/ZF/ex/Acc.thy Wed Jan 13 12:44:33 1999 +0100
+++ b/src/ZF/ex/Acc.thy Wed Jan 13 15:14:47 1999 +0100
@@ -18,6 +18,6 @@
domains "acc(r)" <= "field(r)"
intrs
vimage "[| r-``{a}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"
- monos "[Pow_mono]"
+ monos Pow_mono
end
--- a/src/ZF/ex/Brouwer.thy Wed Jan 13 12:44:33 1999 +0100
+++ b/src/ZF/ex/Brouwer.thy Wed Jan 13 15:14:47 1999 +0100
@@ -15,13 +15,13 @@
datatype <= "Vfrom(0, csucc(nat))"
"brouwer" = Zero | Suc ("b: brouwer") | Lim ("h: nat -> brouwer")
- monos "[Pi_mono]"
+ monos Pi_mono
type_intrs "inf_datatype_intrs"
(*The union with nat ensures that the cardinal is infinite*)
datatype <= "Vfrom(A Un (UN x:A. B(x)), csucc(nat Un |UN x:A. B(x)|))"
"Well(A,B)" = Sup ("a:A", "f: B(a) -> Well(A,B)")
- monos "[Pi_mono]"
+ monos Pi_mono
type_intrs "[[UN_upper_cardinal, le_nat_Un_cardinal] MRS le_trans]
@ inf_datatype_intrs"
--- a/src/ZF/ex/Mutil.thy Wed Jan 13 12:44:33 1999 +0100
+++ b/src/ZF/ex/Mutil.thy Wed Jan 13 15:14:47 1999 +0100
@@ -18,7 +18,7 @@
intrs
horiz "[| i: nat; j: nat |] ==> {<i,j>, <i,succ(j)>} : domino"
vertl "[| i: nat; j: nat |] ==> {<i,j>, <succ(i),j>} : domino"
- type_intrs "[empty_subsetI, cons_subsetI, PowI, SigmaI, nat_succI]"
+ type_intrs empty_subsetI, cons_subsetI, PowI, SigmaI, nat_succI
inductive
@@ -26,7 +26,7 @@
intrs
empty "0 : tiling(A)"
Un "[| a: A; t: tiling(A); a Int t = 0 |] ==> a Un t : tiling(A)"
- type_intrs "[empty_subsetI, Union_upper, Un_least, PowI]"
+ type_intrs empty_subsetI, Union_upper, Un_least, PowI
type_elims "[make_elim PowD]"
constdefs
--- a/src/ZF/ex/Ntree.thy Wed Jan 13 12:44:33 1999 +0100
+++ b/src/ZF/ex/Ntree.thy Wed Jan 13 15:14:47 1999 +0100
@@ -19,16 +19,16 @@
"ntree(A)" = Branch ("a: A", "h: (UN n:nat. n -> ntree(A))")
monos "[[subset_refl, Pi_mono] MRS UN_mono]" (*MUST have this form*)
type_intrs "[nat_fun_univ RS subsetD]"
- type_elims "[UN_E]"
+ type_elims UN_E
datatype
"maptree(A)" = Sons ("a: A", "h: maptree(A) -||> maptree(A)")
- monos "[FiniteFun_mono1]" (*Use monotonicity in BOTH args*)
+ monos FiniteFun_mono1 (*Use monotonicity in BOTH args*)
type_intrs "[FiniteFun_univ1 RS subsetD]"
datatype
"maptree2(A,B)" = Sons2 ("a: A", "h: B -||> maptree2(A,B)")
monos "[subset_refl RS FiniteFun_mono]"
- type_intrs "[FiniteFun_in_univ']"
+ type_intrs FiniteFun_in_univ'
end
--- a/src/ZF/ex/Primrec.thy Wed Jan 13 12:44:33 1999 +0100
+++ b/src/ZF/ex/Primrec.thy Wed Jan 13 15:14:47 1999 +0100
@@ -26,8 +26,8 @@
PROJ "i: nat ==> PROJ(i) : prim_rec"
COMP "[| g: prim_rec; fs: list(prim_rec) |] ==> COMP(g,fs): prim_rec"
PREC "[| f: prim_rec; g: prim_rec |] ==> PREC(f,g): prim_rec"
- monos "[list_mono]"
- con_defs "[SC_def, CONST_def, PROJ_def, COMP_def, PREC_def]"
+ monos list_mono
+ con_defs SC_def, CONST_def, PROJ_def, COMP_def, PREC_def
type_intrs "nat_typechecks @ list.intrs @
[lam_type, list_case_type, drop_type, map_type,
apply_type, rec_type]"
--- a/src/ZF/ex/Term.thy Wed Jan 13 12:44:33 1999 +0100
+++ b/src/ZF/ex/Term.thy Wed Jan 13 15:14:47 1999 +0100
@@ -13,7 +13,7 @@
datatype
"term(A)" = Apply ("a: A", "l: list(term(A))")
- monos "[list_mono]"
+ monos list_mono
type_elims "[make_elim (list_univ RS subsetD)]"
(*Or could have