equal
deleted
inserted
replaced
170 val def_swap_iff = result(); |
170 val def_swap_iff = result(); |
171 |
171 |
172 val def_trans = prove_goal IFOL.thy "[| f==g; g(a)=b |] ==> f(a)=b" |
172 val def_trans = prove_goal IFOL.thy "[| f==g; g(a)=b |] ==> f(a)=b" |
173 (fn [rew,prem] => [ rewtac rew, rtac prem 1 ]); |
173 (fn [rew,prem] => [ rewtac rew, rtac prem 1 ]); |
174 |
174 |
|
175 (*Delete needless equality assumptions*) |
|
176 val refl_thin = prove_goal IFOL.thy "!!P. [| a=a; P |] ==> P" |
|
177 (fn _ => [assume_tac 1]); |
175 |
178 |