equal
deleted
inserted
replaced
134 Sign.string_of_term sign rl); |
134 Sign.string_of_term sign rl); |
135 |
135 |
136 (*For simplifying the elimination rule*) |
136 (*For simplifying the elimination rule*) |
137 val sumprod_free_SEs = |
137 val sumprod_free_SEs = |
138 Pair_inject :: |
138 Pair_inject :: |
139 map make_elim [Inl_neq_Inr, Inr_neq_Inl, Inl_inject, Inr_inject]; |
139 map make_elim [(*Inl_neq_Inr, Inr_neq_Inl, Inl_inject, Inr_inject*)]; |
140 |
140 |
141 (*For deriving cases rules. |
141 (*For deriving cases rules. |
142 read_instantiate replaces a propositional variable by a formula variable*) |
142 read_instantiate replaces a propositional variable by a formula variable*) |
143 val equals_CollectD = |
143 val equals_CollectD = |
144 read_instantiate [("W","?Q")] |
144 read_instantiate [("W","?Q")] |