src/HOL/TPTP/mash_export.ML
changeset 48242 713e32be9845
parent 48240 6a8d18798161
child 48245 854a47677335
equal deleted inserted replaced
48241:688f1172d523 48242:713e32be9845
   177 
   177 
   178 fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1})
   178 fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1})
   179 
   179 
   180 val max_depth = 1
   180 val max_depth = 1
   181 
   181 
       
   182 (* TODO: Generate type classes for types? *)
   182 fun features_of thy (status, th) =
   183 fun features_of thy (status, th) =
   183   let val t = Thm.prop_of th in
   184   let val t = Thm.prop_of th in
   184     thy_name_of (thy_name_of_thm th) ::
   185     thy_name_of (thy_name_of_thm th) ::
   185     interesting_terms_types_and_classes max_depth max_depth t
   186     interesting_terms_types_and_classes max_depth max_depth t
   186     |> not (has_no_lambdas t) ? cons "lambdas"
   187     |> not (has_no_lambdas t) ? cons "lambdas"