equal
deleted
inserted
replaced
51 by (resolve_tac prems 2); |
51 by (resolve_tac prems 2); |
52 by (rtac (cond_1 RS ssubst) 1); |
52 by (rtac (cond_1 RS ssubst) 1); |
53 by (resolve_tac prems 1); |
53 by (resolve_tac prems 1); |
54 val cond_type = result(); |
54 val cond_type = result(); |
55 |
55 |
56 val [cond_cong] = mk_congs Bool.thy ["cond"]; |
|
57 val bool_congs = mk_congs Bool.thy ["cond","not","op and","op or","op xor"]; |
|
58 |
|
59 val [rew] = goal Bool.thy "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c"; |
56 val [rew] = goal Bool.thy "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c"; |
60 by (rewtac rew); |
57 by (rewtac rew); |
61 by (rtac cond_1 1); |
58 by (rtac cond_1 1); |
62 val def_cond_1 = result(); |
59 val def_cond_1 = result(); |
63 |
60 |