321 in map (case_UU_tac rews 1) (nonlazy args) @ [ |
321 in map (case_UU_tac rews 1) (nonlazy args) @ [ |
322 asm_simp_tac (HOLCF_ss addsimps rews) 1] end)) |
322 asm_simp_tac (HOLCF_ss addsimps rews) 1] end)) |
323 (filter (fn (_,args)=>exists is_nonlazy_rec args) cons); |
323 (filter (fn (_,args)=>exists is_nonlazy_rec args) cons); |
324 val copy_rews = copy_strict::copy_apps @ copy_stricts; |
324 val copy_rews = copy_strict::copy_apps @ copy_stricts; |
325 in thy |> Theory.add_path (Sign.base_name dname) |
325 in thy |> Theory.add_path (Sign.base_name dname) |
326 |> (PureThy.add_tthmss o map Attribute.no_attrss) [ |
326 |> (PureThy.add_thmss o map Thm.no_attributes) [ |
327 ("iso_rews" , iso_rews ), |
327 ("iso_rews" , iso_rews ), |
328 ("exhaust" , [exhaust] ), |
328 ("exhaust" , [exhaust] ), |
329 ("casedist" , [casedist]), |
329 ("casedist" , [casedist]), |
330 ("when_rews", when_rews ), |
330 ("when_rews", when_rews ), |
331 ("con_rews", con_rews), |
331 ("con_rews", con_rews), |
596 take_lemmas)); |
596 take_lemmas)); |
597 end; (* local *) |
597 end; (* local *) |
598 |
598 |
599 |
599 |
600 in thy |> Theory.add_path comp_dnam |
600 in thy |> Theory.add_path comp_dnam |
601 |> (PureThy.add_tthmss o map Attribute.no_attrss) [ |
601 |> (PureThy.add_thmss o map Thm.no_attributes) [ |
602 ("take_rews" , take_rews ), |
602 ("take_rews" , take_rews ), |
603 ("take_lemmas", take_lemmas), |
603 ("take_lemmas", take_lemmas), |
604 ("finites" , finites ), |
604 ("finites" , finites ), |
605 ("finite_ind", [finite_ind]), |
605 ("finite_ind", [finite_ind]), |
606 ("ind" , [ind ]), |
606 ("ind" , [ind ]), |