author | huffman |
Mon, 12 Sep 2005 23:18:01 +0200 | |
changeset 17333 | 605c97701833 |
parent 17332 | 4910cf8c0cd2 |
child 17334 | 6e5815f4d770 |
--- a/src/HOL/Hyperreal/transfer.ML Mon Sep 12 23:14:41 2005 +0200 +++ b/src/HOL/Hyperreal/transfer.ML Mon Sep 12 23:18:01 2005 +0200 @@ -1,3 +1,10 @@ +(* Title : HOL/Hyperreal/transfer.ML + ID : $Id$ + Author : Brian Huffman + +Transfer principle tactic for nonstandard analysis +*) + signature TRANSFER_TAC = sig val transfer_tac: thm list -> int -> tactic