# HG changeset patch
# User paulson
# Date 916236887 -3600
# Node ID f9aad8ccd59067b82870d7cbde0d7d76874c9a48
# Parent  8ba2f25610f70f3d8e709a8f5d76478404352c1a
tidying of datatype and inductive definitions

diff -r 8ba2f25610f7 -r f9aad8ccd590 src/ZF/Coind/ECR.thy
--- 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 *)
diff -r 8ba2f25610f7 -r f9aad8ccd590 src/ZF/Coind/Values.thy
--- 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
diff -r 8ba2f25610f7 -r f9aad8ccd590 src/ZF/Integ/Bin.thy
--- 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)"
diff -r 8ba2f25610f7 -r f9aad8ccd590 src/ZF/ex/Acc.thy
--- 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
diff -r 8ba2f25610f7 -r f9aad8ccd590 src/ZF/ex/Brouwer.thy
--- 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"
 
diff -r 8ba2f25610f7 -r f9aad8ccd590 src/ZF/ex/Mutil.thy
--- 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
diff -r 8ba2f25610f7 -r f9aad8ccd590 src/ZF/ex/Ntree.thy
--- 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
diff -r 8ba2f25610f7 -r f9aad8ccd590 src/ZF/ex/Primrec.thy
--- 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]"
diff -r 8ba2f25610f7 -r f9aad8ccd590 src/ZF/ex/Term.thy
--- 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