changeset 5530 | c361279ebc66 |
parent 5268 | 59ef39008514 |
child 6046 | 2c8a8be36c94 |
--- a/src/ZF/ex/BT.ML Tue Sep 22 13:50:57 1998 +0200 +++ b/src/ZF/ex/BT.ML Tue Sep 22 15:22:18 1998 +0200 @@ -52,7 +52,7 @@ Goal "bt_rec(Br(a,l,r), c, h) = h(a, l, r, bt_rec(l,c,h), bt_rec(r,c,h))"; by (rtac (bt_rec_def RS def_Vrec RS trans) 1); -by (simp_tac (rank_ss addsimps (bt.case_eqns @ [rank_Br1, rank_Br2])) 1); +by (simp_tac (rank_ss addsimps bt.case_eqns @ [rank_Br1, rank_Br2]) 1); qed "bt_rec_Br"; Addsimps [bt_rec_Lf, bt_rec_Br];