src/HOL/Tools/Quotient/quotient_term.ML
changeset 35788 f1deaca15ca3
parent 35402 115a5a95710a
child 35843 23908b4dbc2f
     1.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Sun Mar 14 14:29:30 2010 +0100
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Sun Mar 14 14:31:24 2010 +0100
     1.3 @@ -1,8 +1,8 @@
     1.4 -(*  Title:      quotient_term.thy
     1.5 +(*  Title:      HOL/Tools/Quotient/quotient_term.thy
     1.6      Author:     Cezary Kaliszyk and Christian Urban
     1.7  
     1.8 -    Constructs terms corresponding to goals from
     1.9 -    lifting theorems to quotient types.
    1.10 +Constructs terms corresponding to goals from lifting theorems to
    1.11 +quotient types.
    1.12  *)
    1.13  
    1.14  signature QUOTIENT_TERM =
    1.15 @@ -779,8 +779,4 @@
    1.16    lift_aux t
    1.17  end
    1.18  
    1.19 -
    1.20  end; (* structure *)
    1.21 -
    1.22 -
    1.23 -