Removed (Unit) in Prod.
authornipkow
Thu Apr 03 09:46:42 1997 +0200 (1997-04-03)
changeset 2880a0fde30aa126
parent 2879 477bfcb022d8
child 2881 62ecde1015ae
Removed (Unit) in Prod.
Added test for ancestor Nat in datatype.
src/HOL/Prod.ML
src/HOL/Prod.thy
src/HOL/datatype.ML
     1.1 --- a/src/HOL/Prod.ML	Wed Apr 02 19:12:26 1997 +0200
     1.2 +++ b/src/HOL/Prod.ML	Thu Apr 03 09:46:42 1997 +0200
     1.3 @@ -302,8 +302,8 @@
     1.4  
     1.5  goalw Prod.thy [Unity_def]
     1.6      "u = ()";
     1.7 -by (stac (rewrite_rule [Unit_def] Rep_Unit RS CollectD RS sym) 1);
     1.8 -by (rtac (Rep_Unit_inverse RS sym) 1);
     1.9 +by (stac (rewrite_rule [unit_def] Rep_unit RS CollectD RS sym) 1);
    1.10 +by (rtac (Rep_unit_inverse RS sym) 1);
    1.11  qed "unit_eq";
    1.12   
    1.13  AddIs  [fst_imageI, snd_imageI, prod_fun_imageI];
     2.1 --- a/src/HOL/Prod.thy	Wed Apr 02 19:12:26 1997 +0200
     2.2 +++ b/src/HOL/Prod.thy	Thu Apr 03 09:46:42 1997 +0200
     2.3 @@ -79,14 +79,13 @@
     2.4  
     2.5  (** unit **)
     2.6  
     2.7 -typedef (Unit)
     2.8 -  unit = "{p. p = True}"
     2.9 +typedef  unit = "{p. p = True}"
    2.10  
    2.11  consts
    2.12    "()"          :: unit                           ("'(')")
    2.13  
    2.14  defs
    2.15 -  Unity_def     "() == Abs_Unit True"
    2.16 +  Unity_def     "() == Abs_unit True"
    2.17  
    2.18  end
    2.19  
     3.1 --- a/src/HOL/datatype.ML	Wed Apr 02 19:12:26 1997 +0200
     3.2 +++ b/src/HOL/datatype.ML	Thu Apr 03 09:46:42 1997 +0200
     3.3 @@ -138,6 +138,9 @@
     3.4  in
     3.5    fun add_datatype (typevars, tname, cons_list') thy = 
     3.6      let
     3.7 +      val dummy = if length cons_list' < dtK then ()
     3.8 +                  else require_thy thy "Nat" "datatype";
     3.9 +      
    3.10        fun typid(dtRek(_,id)) = id
    3.11          | typid(dtVar s) = implode (tl (explode s))
    3.12          | typid(dtTyp(_,id)) = id;