src/HOL/Reconstruction.thy
changeset 15645 5e20c54683d3
parent 15382 e56ce5cefe9c
child 15653 3549ff7158f3
equal deleted inserted replaced
15644:f2ef8c258fa4 15645:5e20c54683d3
    11     files "Tools/res_lib.ML"
    11     files "Tools/res_lib.ML"
    12 	  "Tools/res_clause.ML"
    12 	  "Tools/res_clause.ML"
    13 	  "Tools/res_skolem_function.ML"
    13 	  "Tools/res_skolem_function.ML"
    14 	  "Tools/res_axioms.ML"
    14 	  "Tools/res_axioms.ML"
    15 	  "Tools/res_types_sorts.ML"
    15 	  "Tools/res_types_sorts.ML"
    16 	  "Tools/res_atp.ML"
       
    17           "Tools/reconstruction.ML"
    16           "Tools/reconstruction.ML"
    18 
    17 
    19 begin
    18 begin
    20 
    19 
    21 text{*Every theory of HOL must be a descendant or ancestor of this one!*}
    20 text{*Every theory of HOL must be a descendant or ancestor of this one!*}