src/HOL/Tools/meson.ML
changeset 13105 3d1e7a199bdc
parent 12299 2c76042c3b06
child 14733 3eda95792083
equal deleted inserted replaced
13104:df7aac8543c9 13105:3d1e7a199bdc
   264     sort_clauses (map (generalize o nodups) (foldr cnf (ths,[])));
   264     sort_clauses (map (generalize o nodups) (foldr cnf (ths,[])));
   265 
   265 
   266 (*Convert a list of clauses to (contrapositive) Horn clauses*)
   266 (*Convert a list of clauses to (contrapositive) Horn clauses*)
   267 fun make_horns ths =
   267 fun make_horns ths =
   268     name_thms "Horn#"
   268     name_thms "Horn#"
   269       (gen_distinct eq_thm (foldr (add_contras clause_rules) (ths,[])));
   269       (gen_distinct Drule.eq_thm_prop (foldr (add_contras clause_rules) (ths,[])));
   270 
   270 
   271 (*Could simply use nprems_of, which would count remaining subgoals -- no
   271 (*Could simply use nprems_of, which would count remaining subgoals -- no
   272   discrimination as to their size!  With BEST_FIRST, fails for problem 41.*)
   272   discrimination as to their size!  With BEST_FIRST, fails for problem 41.*)
   273 
   273 
   274 fun best_prolog_tac sizef horns =
   274 fun best_prolog_tac sizef horns =