src/HOL/Prod.thy
changeset 1454 d0266c81a85e
parent 1370 7361ac9b024d
child 1475 7f5a4cd08209
     1.1 --- a/src/HOL/Prod.thy	Fri Jan 26 13:43:36 1996 +0100
     1.2 +++ b/src/HOL/Prod.thy	Fri Jan 26 20:25:39 1996 +0100
     1.3 @@ -50,8 +50,6 @@
     1.4  
     1.5    "%(x,y,zs).b"   == "split(%x (y,zs).b)"
     1.6    "%(x,y).b"      == "split(%x y.b)"
     1.7 -(* The <= direction fails if split has more than one argument because
     1.8 -   ast-matching fails. Otherwise it would work fine *)
     1.9  
    1.10  defs
    1.11    Pair_def      "Pair a b == Abs_Prod(Pair_Rep a b)"
    1.12 @@ -61,8 +59,6 @@
    1.13    prod_fun_def  "prod_fun f g == split(%x y.(f(x), g(y)))"
    1.14    Sigma_def     "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
    1.15  
    1.16 -
    1.17 -
    1.18  (** Unit **)
    1.19  
    1.20  subtype (Unit)
    1.21 @@ -78,31 +74,3 @@
    1.22  (* end 8bit 1 *)
    1.23  
    1.24  end
    1.25 -(*
    1.26 -ML
    1.27 -
    1.28 -local open Syntax
    1.29 -
    1.30 -fun pttrn(_ $ s $ t) = const"@pttrn" $ s $ t;
    1.31 -fun pttrns s t = const"@pttrns" $ s $ t;
    1.32 -
    1.33 -fun split2(Abs(x,T,t)) =
    1.34 -      let val (pats,u) = split1 t
    1.35 -      in (pttrns (Free(x,T)) pats, subst_bounds([free x],u)) end
    1.36 -  | split2(Const("split",_) $ r) =
    1.37 -      let val (pats,s) = split2(r)
    1.38 -          val (pats2,t) = split1(s)
    1.39 -      in (pttrns (pttrn pats) pats2, t) end
    1.40 -and split1(Abs(x,T,t)) =  (Free(x,T), subst_bounds([free x],t))
    1.41 -  | split1(Const("split",_)$t) = split2(t);
    1.42 -
    1.43 -fun split_tr'(t::args) =
    1.44 -  let val (pats,ft) = split2(t)
    1.45 -  in list_comb(const"_lambda" $ pttrn pats $ ft, args) end;
    1.46 -
    1.47 -in
    1.48 -
    1.49 -val print_translation = [("split", split_tr')];
    1.50 -
    1.51 -end;
    1.52 -*)