src/HOL/Lifting.thy
changeset 58177 166131276380
parent 57961 10b2f60b70f0
child 58186 a6c3962ea907
     1.1 --- a/src/HOL/Lifting.thy	Wed Sep 03 22:47:48 2014 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Wed Sep 03 22:49:05 2014 +0200
     1.3 @@ -556,11 +556,8 @@
     1.4  lemmas [relator_distr] = pos_fun_distr neg_fun_distr1 neg_fun_distr2
     1.5  
     1.6  ML_file "Tools/Lifting/lifting_bnf.ML"
     1.7 -
     1.8  ML_file "Tools/Lifting/lifting_term.ML"
     1.9 -
    1.10  ML_file "Tools/Lifting/lifting_def.ML"
    1.11 -
    1.12  ML_file "Tools/Lifting/lifting_setup.ML"
    1.13                             
    1.14  hide_const (open) POS NEG