| changeset 4833 | 2e53109d4bc8 |
| parent 4642 | 2d3910d6ab10 |
| child 5068 | fb28eaa07e01 |
--- a/src/HOLCF/Tr.ML Mon Apr 27 16:46:56 1998 +0200 +++ b/src/HOLCF/Tr.ML Mon Apr 27 16:47:50 1998 +0200 @@ -99,10 +99,10 @@ "P (If2 Q x y ) = ((Q=UU --> P UU) & (Q=TT --> P x) & (Q=FF --> P y))"; by (res_inst_tac [("p","Q")] trE 1); by (REPEAT (Asm_full_simp_tac 1)); -qed"expand_If2"; +qed"split_If2"; val split_If_tac = - simp_tac (HOL_basic_ss addsimps [symmetric If2_def]) THEN' (split_tac [expand_If2]); + simp_tac (HOL_basic_ss addsimps [symmetric If2_def]) THEN' (split_tac [split_If2]);