equal
deleted
inserted
replaced
120 (*Delete needless equality assumptions*) |
120 (*Delete needless equality assumptions*) |
121 val refl_thin = prove_goal HOL.thy "!!P. [| a=a; P |] ==> P" |
121 val refl_thin = prove_goal HOL.thy "!!P. [| a=a; P |] ==> P" |
122 (fn _ => [assume_tac 1]); |
122 (fn _ => [assume_tac 1]); |
123 |
123 |
124 (*Includes rules for Suc and Pair since they are common constructions*) |
124 (*Includes rules for Suc and Pair since they are common constructions*) |
125 val elim_rls = [asm_rl, FalseE, Suc_neq_Zero, Zero_neq_Suc, |
125 val elim_rls = [asm_rl, FalseE, (*Suc_neq_Zero, Zero_neq_Suc, |
126 make_elim Suc_inject, |
126 make_elim Suc_inject, *) |
127 refl_thin, conjE, exE, disjE]; |
127 refl_thin, conjE, exE, disjE]; |
128 |
128 |
129 end; |
129 end; |