equal
deleted
inserted
replaced
2 Author: Brian Huffman |
2 Author: Brian Huffman |
3 |
3 |
4 Transfer principle tactic for nonstandard analysis. |
4 Transfer principle tactic for nonstandard analysis. |
5 *) |
5 *) |
6 |
6 |
7 signature TRANSFER = |
7 signature TRANSFER_PRINCIPLE = |
8 sig |
8 sig |
9 val transfer_tac: Proof.context -> thm list -> int -> tactic |
9 val transfer_tac: Proof.context -> thm list -> int -> tactic |
10 val add_const: string -> theory -> theory |
10 val add_const: string -> theory -> theory |
11 val setup: theory -> theory |
11 val setup: theory -> theory |
12 end; |
12 end; |
13 |
13 |
14 structure Transfer: TRANSFER = |
14 structure Transfer_Principle: TRANSFER_PRINCIPLE = |
15 struct |
15 struct |
16 |
16 |
17 structure TransferData = Generic_Data |
17 structure TransferData = Generic_Data |
18 ( |
18 ( |
19 type T = { |
19 type T = { |