src/HOL/Wellfounded.thy
changeset 48891 c0eafbd55de3
parent 47433 07f4bf913230
child 49945 fb696ff1f086
     1.1 --- a/src/HOL/Wellfounded.thy	Wed Aug 22 22:47:16 2012 +0200
     1.2 +++ b/src/HOL/Wellfounded.thy	Wed Aug 22 22:55:41 2012 +0200
     1.3 @@ -9,7 +9,6 @@
     1.4  
     1.5  theory Wellfounded
     1.6  imports Transitive_Closure
     1.7 -uses ("Tools/Function/size.ML")
     1.8  begin
     1.9  
    1.10  subsection {* Basic Definitions *}
    1.11 @@ -845,8 +844,7 @@
    1.12  
    1.13  subsection {* size of a datatype value *}
    1.14  
    1.15 -use "Tools/Function/size.ML"
    1.16 -
    1.17 +ML_file "Tools/Function/size.ML"
    1.18  setup Size.setup
    1.19  
    1.20  lemma size_bool [code]: