author | paulson |
Tue, 22 Sep 1998 15:22:18 +0200 | |
changeset 5530 | c361279ebc66 |
parent 5529 | 4a54acae6a15 |
child 5531 | 75356cabe3bb |
src/ZF/ex/BT.ML | file | annotate | diff | comparison | revisions |
--- 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];