src/HOL/Tools/Quotient/quotient_tacs.ML
changeset 37744 3daaf23b9ab4
parent 37593 2505feaf2d70
child 38317 cb8e2ac6397b
equal deleted inserted replaced
37743:0a3fa8fbcdc5 37744:3daaf23b9ab4
     1 (*  Title:      HOL/Tools/Quotient/quotient_tacs.thy
     1 (*  Title:      HOL/Tools/Quotient/quotient_tacs.ML
     2     Author:     Cezary Kaliszyk and Christian Urban
     2     Author:     Cezary Kaliszyk and Christian Urban
     3 
     3 
     4 Tactics for solving goal arising from lifting theorems to quotient
     4 Tactics for solving goal arising from lifting theorems to quotient
     5 types.
     5 types.
     6 *)
     6 *)