# HG changeset patch
# User huffman
# Date 1187905071 -7200
# Node ID 5c3858b71f802c0831ccc85e4dbca9484662ea23
# Parent  0ca0c958c43457c61ca2fed075710ce82ac6cf83
remove lemma bin_rec_PM

diff -r 0ca0c958c434 -r 5c3858b71f80 src/HOL/Word/BinGeneral.thy
--- a/src/HOL/Word/BinGeneral.thy	Thu Aug 23 23:34:51 2007 +0200
+++ b/src/HOL/Word/BinGeneral.thy	Thu Aug 23 23:37:51 2007 +0200
@@ -64,15 +64,11 @@
   bin_rec :: "'a => 'a => (int => bit => 'a => 'a) => int => 'a"
   "bin_rec f1 f2 f3 bin == bin_rec' (bin, f1, f2, f3)"
 
-lemma bin_rec_PM:
-  "f = bin_rec f1 f2 f3 ==> f Numeral.Pls = f1 & f Numeral.Min = f2"
-  apply safe
-   apply (unfold bin_rec_def)
-   apply (auto intro: bin_rec'.simps [THEN trans])
-  done
+lemma bin_rec_Pls: "bin_rec f1 f2 f3 Numeral.Pls = f1"
+  unfolding bin_rec_def by simp
 
-lemmas bin_rec_Pls = refl [THEN bin_rec_PM, THEN conjunct1, standard]
-lemmas bin_rec_Min = refl [THEN bin_rec_PM, THEN conjunct2, standard]
+lemma bin_rec_Min: "bin_rec f1 f2 f3 Numeral.Min = f2"
+  unfolding bin_rec_def by simp
 
 lemma bin_rec_Bit:
   "f = bin_rec f1 f2 f3  ==> f3 Numeral.Pls bit.B0 f1 = f1 ==>