equal
deleted
inserted
replaced
5 Description: Embedding the integers in the reals |
5 Description: Embedding the integers in the reals |
6 *) |
6 *) |
7 |
7 |
8 |
8 |
9 Goalw [congruent_def] |
9 Goalw [congruent_def] |
10 "congruent intrel (%p. split (%i j. realrel ^^ \ |
10 "congruent intrel (%p. (%(i,j). realrel ^^ \ |
11 \ {(preal_of_prat (prat_of_pnat (pnat_of_nat i)), \ |
11 \ {(preal_of_prat (prat_of_pnat (pnat_of_nat i)), \ |
12 \ preal_of_prat (prat_of_pnat (pnat_of_nat j)))}) p)"; |
12 \ preal_of_prat (prat_of_pnat (pnat_of_nat j)))}) p)"; |
13 by (auto_tac (claset(), |
13 by (auto_tac (claset(), |
14 simpset() addsimps [pnat_of_nat_add, prat_of_pnat_add RS sym, |
14 simpset() addsimps [pnat_of_nat_add, prat_of_pnat_add RS sym, |
15 preal_of_prat_add RS sym])); |
15 preal_of_prat_add RS sym])); |