equal
deleted
inserted
replaced
44 |
44 |
45 (* inductive_cases command *) |
45 (* inductive_cases command *) |
46 |
46 |
47 fun inductive_cases args thy = |
47 fun inductive_cases args thy = |
48 let |
48 let |
49 val ctxt = ProofContext.init thy; |
49 val ctxt = ProofContext.init_global thy; |
50 val facts = args |> map (fn ((name, srcs), props) => |
50 val facts = args |> map (fn ((name, srcs), props) => |
51 ((name, map (Attrib.attribute thy) srcs), |
51 ((name, map (Attrib.attribute thy) srcs), |
52 map (Thm.no_attributes o single o smart_cases ctxt) props)); |
52 map (Thm.no_attributes o single o smart_cases ctxt) props)); |
53 in thy |> PureThy.note_thmss "" facts |> snd end; |
53 in thy |> PureThy.note_thmss "" facts |> snd end; |
54 |
54 |