src/HOL/Quotient_Examples/Int_Pow.thy
changeset 66453 cc19f7ca2ed6
parent 63540 f8652d0534fa
child 67341 df79ef3b3a41
equal deleted inserted replaced
66452:450cefec7c11 66453:cc19f7ca2ed6
     2     Author:     Ondrej Kuncar
     2     Author:     Ondrej Kuncar
     3     Author:     Lars Noschinski
     3     Author:     Lars Noschinski
     4 *)
     4 *)
     5 
     5 
     6 theory Int_Pow
     6 theory Int_Pow
     7 imports Main "~~/src/HOL/Algebra/Group"
     7 imports Main "HOL-Algebra.Group"
     8 begin
     8 begin
     9 
     9 
    10 (*
    10 (*
    11   This file demonstrates how to restore Lifting/Transfer enviromenent.
    11   This file demonstrates how to restore Lifting/Transfer enviromenent.
    12 
    12