changeset 35788 | f1deaca15ca3 |
parent 35625 | 9c818cab0dd0 |
child 35789 | a2b163256f9b |
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Sun Mar 14 14:29:30 2010 +0100 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Sun Mar 14 14:31:24 2010 +0100 @@ -1,8 +1,8 @@ -(* Title: quotient_tacs.thy +(* Title: HOL/Tools/Quotient/quotient_tacs.thy Author: Cezary Kaliszyk and Christian Urban - Tactics for solving goal arising from lifting - theorems to quotient types. +Tactics for solving goal arising from lifting theorems to quotient +types. *) signature QUOTIENT_TACS =