src/HOL/Record.thy
changeset 13421 8fcdf4a26468
parent 13412 666137b488a4
child 14080 9a50427d7165
     1.1 --- a/src/HOL/Record.thy	Wed Jul 24 22:14:42 2002 +0200
     1.2 +++ b/src/HOL/Record.thy	Wed Jul 24 22:15:55 2002 +0200
     1.3 @@ -18,9 +18,6 @@
     1.4      and dest1: "dest1 == (\<lambda>p. fst (Rep p))"
     1.5      and dest2: "dest2 == (\<lambda>p. snd (Rep p))"
     1.6  
     1.7 -lemmas product_typeI =
     1.8 -  product_type.intro [OF product_type_axioms.intro]
     1.9 -
    1.10  lemma (in product_type)
    1.11      "inject": "(pair x y = pair x' y') = (x = x' \<and> y = y')"
    1.12    by (simp add: pair type_definition.Abs_inject [OF "typedef"])