src/Pure/meta_simplifier.ML
changeset 15088 b8a95eadbc14
parent 15034 e1282c4b39be
child 15195 197e00ce3f20
equal deleted inserted replaced
15087:666f89fbb860 15088:b8a95eadbc14
   283       |> Library.sort_wrt #1;
   283       |> Library.sort_wrt #1;
   284   in
   284   in
   285     [Pretty.big_list "simplification rules:" (pretty_thms smps),
   285     [Pretty.big_list "simplification rules:" (pretty_thms smps),
   286       Pretty.big_list "simplification procedures:" (map pretty_proc prcs),
   286       Pretty.big_list "simplification procedures:" (map pretty_proc prcs),
   287       Pretty.big_list "congruences:" (map pretty_cong cngs),
   287       Pretty.big_list "congruences:" (map pretty_cong cngs),
   288       Pretty.strs ("loopers:" :: map #1 loop_tacs),
   288       Pretty.strs ("loopers:" :: map (quote o #1) loop_tacs),
   289       Pretty.strs ("unsafe solvers:" :: map solver_name (#1 solvers)),
   289       Pretty.strs ("unsafe solvers:" :: map (quote o solver_name) (#1 solvers)),
   290       Pretty.strs ("safe solvers:" :: map solver_name (#2 solvers))]
   290       Pretty.strs ("safe solvers:" :: map (quote o solver_name) (#2 solvers))]
   291     |> Pretty.chunks |> Pretty.writeln
   291     |> Pretty.chunks |> Pretty.writeln
   292   end;
   292   end;
   293 
   293 
   294 
   294 
   295 (* empty simpsets *)
   295 (* empty simpsets *)