# HG changeset patch
# User haftmann
# Date 1206010972 -3600
# Node ID 2312df2efa125e200ec23ca38e79315d7521f972
# Parent  9276633fdc246e99c44c3288e8c5e267c2b14c4c
Product_Type.apfst and Product_Type.apsnd

diff -r 9276633fdc24 -r 2312df2efa12 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Thu Mar 20 12:02:51 2008 +0100
+++ b/src/HOL/Datatype.thy	Thu Mar 20 12:02:52 2008 +0100
@@ -28,7 +28,6 @@
       ('a, 'b) dtree = "('a, 'b) node set"
 
 consts
-  apfst     :: "['a=>'c, 'a*'b] => 'c*'b"
   Push      :: "[('b + nat), nat => ('b + nat)] => (nat => ('b + nat))"
 
   Push_Node :: "[('b + nat), ('a, 'b) node] => ('a, 'b) node"
@@ -61,7 +60,6 @@
   Push_Node_def:  "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
 
   (*crude "lists" of nats -- needed for the constructions*)
-  apfst_def:  "apfst == (%f (x,y). (f(x),y))"
   Push_def:   "Push == (%b h. nat_case b h)"
 
   (** operations on S-expressions -- sets of nodes **)
@@ -105,12 +103,6 @@
 
 
 
-(** apfst -- can be used in similar type definitions **)
-
-lemma apfst_conv [simp, code]: "apfst f (a, b) = (f a, b)"
-by (simp add: apfst_def)
-
-
 lemma apfst_convE: 
     "[| q = apfst f p;  !!x y. [| p = (x,y);  q = (f(x),y) |] ==> R  
      |] ==> R"