| changeset 17333 | 605c97701833 |
| parent 17332 | 4910cf8c0cd2 |
| child 17429 | e8d6ed3aacfe |
| 17332:4910cf8c0cd2 | 17333:605c97701833 |
|---|---|
1 (* Title : HOL/Hyperreal/transfer.ML |
|
2 ID : $Id$ |
|
3 Author : Brian Huffman |
|
4 |
|
5 Transfer principle tactic for nonstandard analysis |
|
6 *) |
|
7 |
|
1 signature TRANSFER_TAC = |
8 signature TRANSFER_TAC = |
2 sig |
9 sig |
3 val transfer_tac: thm list -> int -> tactic |
10 val transfer_tac: thm list -> int -> tactic |
4 val setup: (theory -> theory) list |
11 val setup: (theory -> theory) list |
5 end; |
12 end; |