--- 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"