src/ZF/Tools/ind_cases.ML
changeset 20916 ee6e3597bb4d
parent 20342 4392003fcbfa
child 21879 a3efbae45735
equal deleted inserted replaced
20915:dcb0a3e2f1bd 20916:ee6e3597bb4d
    53     val read_prop = ProofContext.read_prop (ProofContext.init thy);
    53     val read_prop = ProofContext.read_prop (ProofContext.init thy);
    54     val mk_cases = smart_cases thy (Simplifier.simpset_of thy) read_prop;
    54     val mk_cases = smart_cases thy (Simplifier.simpset_of thy) read_prop;
    55     val facts = args |> map (fn ((name, srcs), props) =>
    55     val facts = args |> map (fn ((name, srcs), props) =>
    56       ((name, map (Attrib.attribute thy) srcs),
    56       ((name, map (Attrib.attribute thy) srcs),
    57         map (Thm.no_attributes o single o mk_cases) props));
    57         map (Thm.no_attributes o single o mk_cases) props));
    58   in thy |> IsarThy.theorems_i PureThy.lemmaK facts |> snd end;
    58   in thy |> PureThy.note_thmss_i "" facts |> snd end;
    59 
    59 
    60 
    60 
    61 (* ind_cases method *)
    61 (* ind_cases method *)
    62 
    62 
    63 fun mk_cases_meth (ctxt, props) =
    63 fun mk_cases_meth (ctxt, props) =