src/HOL/Tools/TFL/casesplit.ML
changeset 32091 30e2ffbba718
parent 32035 8e77b6a250d5
child 32712 ec5976f4d3d8
equal deleted inserted replaced
32090:39acf19e9f3a 32091:30e2ffbba718
   267           Thm.biresolution false [(false,split)] 1 th;
   267           Thm.biresolution false [(false,split)] 1 th;
   268 
   268 
   269       fun split th =
   269       fun split th =
   270           (case find_thms_split splitths 1 th of
   270           (case find_thms_split splitths 1 th of
   271              NONE =>
   271              NONE =>
   272              (writeln "th:";
   272              (writeln (cat_lines
   273               Display.print_thm th; writeln "split ths:";
   273               (["th:", Display.string_of_thm_without_context th, "split ths:"] @
   274               Display.print_thms splitths; writeln "\n--";
   274                 map Display.string_of_thm_without_context splitths @ ["\n--"]));
   275               error "splitto: cannot find variable to split on")
   275               error "splitto: cannot find variable to split on")
   276             | SOME v =>
   276             | SOME v =>
   277              let
   277              let
   278                val gt = Data.dest_Trueprop (List.nth(Thm.prems_of th, 0));
   278                val gt = Data.dest_Trueprop (List.nth(Thm.prems_of th, 0));
   279                val split_thm = mk_casesplit_goal_thm sgn v gt;
   279                val split_thm = mk_casesplit_goal_thm sgn v gt;