equal
deleted
inserted
replaced
213 |> Conjunction.intr_balanced |
213 |> Conjunction.intr_balanced |
214 |> f |
214 |> f |
215 |> Conjunction.elim_balanced (length thms) |
215 |> Conjunction.elim_balanced (length thms) |
216 in |
216 in |
217 thms |
217 thms |
218 |> burrow_thms (canonical_tvars thy purify_tvar) |
|
219 |> map (canonical_vars thy purify_var) |
218 |> map (canonical_vars thy purify_var) |
220 |> map (canonical_absvars purify_var) |
219 |> map (canonical_absvars purify_var) |
|
220 |> map Drule.zero_var_indexes |
|
221 |> burrow_thms (canonical_tvars thy purify_tvar) |
221 |> Drule.zero_var_indexes_list |
222 |> Drule.zero_var_indexes_list |
222 end; |
223 end; |
223 |
224 |
224 |
225 |
225 (* const aliasses *) |
226 (* const aliasses *) |