summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/ZF/OrderArith.ML

changeset 1957 | 58b60b558e48 |

parent 1461 | 6bcb44e4d6e5 |

child 2469 | b50b8c0eec01 |

equal
deleted
inserted
replaced

1956:589af052bcd4 | 1957:58b60b558e48 |
---|---|

77 goal OrderArith.thy |
77 goal OrderArith.thy |

78 "!!r s. [| wf[A](r); wf[B](s) |] ==> wf[A+B](radd(A,r,B,s))"; |
78 "!!r s. [| wf[A](r); wf[B](s) |] ==> wf[A+B](radd(A,r,B,s))"; |

79 by (rtac wf_onI2 1); |
79 by (rtac wf_onI2 1); |

80 by (subgoal_tac "ALL x:A. Inl(x): Ba" 1); |
80 by (subgoal_tac "ALL x:A. Inl(x): Ba" 1); |

81 (*Proving the lemma, which is needed twice!*) |
81 (*Proving the lemma, which is needed twice!*) |

82 by (eres_inst_tac [("V", "y : A + B")] thin_rl 2); |
82 by (thin_tac "y : A + B" 2); |

83 by (rtac ballI 2); |
83 by (rtac ballI 2); |

84 by (eres_inst_tac [("r","r"),("a","x")] wf_on_induct 2 THEN assume_tac 2); |
84 by (eres_inst_tac [("r","r"),("a","x")] wf_on_induct 2 THEN assume_tac 2); |

85 by (etac (bspec RS mp) 2); |
85 by (etac (bspec RS mp) 2); |

86 by (fast_tac sum_cs 2); |
86 by (fast_tac sum_cs 2); |

87 by (best_tac (sum_cs addSEs [raddE]) 2); |
87 by (best_tac (sum_cs addSEs [raddE]) 2); |