equal
deleted
inserted
replaced
99 by (rtac impI 1); |
99 by (rtac impI 1); |
100 by (eresolve_tac prems 1); |
100 by (eresolve_tac prems 1); |
101 by (blast_tac (claset() addIs (prems RL [subsetD])) 1); |
101 by (blast_tac (claset() addIs (prems RL [subsetD])) 1); |
102 qed "wf_induct2"; |
102 qed "wf_induct2"; |
103 |
103 |
104 Goal "!!r A. field(r Int A*A) <= A"; |
104 Goal "field(r Int A*A) <= A"; |
105 by (Blast_tac 1); |
105 by (Blast_tac 1); |
106 qed "field_Int_square"; |
106 qed "field_Int_square"; |
107 |
107 |
108 val wfr::amem::prems = Goalw [wf_on_def] |
108 val wfr::amem::prems = Goalw [wf_on_def] |
109 "[| wf[A](r); a:A; \ |
109 "[| wf[A](r); a:A; \ |