# HG changeset patch # User traytel # Date 1459406330 -7200 # Node ID 596baa1a32517e7749b3192e4b94362d356c3edc # Parent 42a997773bb0b3529228cba06e1c0a6b792097e8 tuned interface diff -r 42a997773bb0 -r 596baa1a3251 src/HOL/BNF_Composition.thy --- a/src/HOL/BNF_Composition.thy Wed Mar 30 23:47:12 2016 +0200 +++ b/src/HOL/BNF_Composition.thy Thu Mar 31 08:38:50 2016 +0200 @@ -81,9 +81,6 @@ lemma Collect_inj: "Collect P = Collect Q \ P = Q" by blast -lemma Ball_Collect: "Ball A P = (A \ (Collect P))" -by auto - lemma Grp_fst_snd: "(Grp (Collect (case_prod R)) fst)^--1 OO Grp (Collect (case_prod R)) snd = R" unfolding Grp_def fun_eq_iff relcompp.simps by auto diff -r 42a997773bb0 -r 596baa1a3251 src/HOL/Tools/BNF/bnf_lift.ML --- a/src/HOL/Tools/BNF/bnf_lift.ML Wed Mar 30 23:47:12 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_lift.ML Thu Mar 31 08:38:50 2016 +0200 @@ -20,8 +20,8 @@ string) * (Facts.ref * Token.src list) option) * (binding * binding * binding) -> local_theory -> local_theory val lift_bnf: - (((lift_bnf_option list * (binding option * (string * sort option)) list) * - string) * thm option) * (binding * binding * binding) -> + ((((lift_bnf_option list * (binding option * (string * sort option)) list) * + string) * term list option) * thm option) * (binding * binding * binding) -> ({context: Proof.context, prems: thm list} -> tactic) list -> local_theory -> local_theory val lift_bnf_cmd: @@ -378,7 +378,7 @@ (fn (goals, after_qed, _, lthy) => lthy |> after_qed (map2 (single oo Goal.prove lthy [] []) goals (tacs (length goals)))) oo - prepare_common prepare_name prepare_typ prepare_sort prepare_thm o apfst (apfst (rpair NONE)); + prepare_common prepare_name prepare_typ prepare_sort prepare_thm; in @@ -387,14 +387,17 @@ (fst o dest_Type oo Proof_Context.read_type_name {proper = true, strict = false}) Syntax.read_sort Syntax.read_term (singleton o Attrib.eval_thms); -fun lift_bnf args tacs = prepare_solve (K I) (K I) (K I) (K I) (K tacs) args; +fun lift_bnf args tacs = + prepare_solve (K I) (K I) (K I) (K I) (K tacs) args; val copy_bnf = - prepare_solve (K I) (K I) (K I) (K I) + apfst (apfst (rpair NONE)) + #> prepare_solve (K I) (K I) (K I) (K I) (fn n => replicate n (fn {context = ctxt, prems = _} => rtac ctxt UNIV_I 1)); val copy_bnf_cmd = - prepare_solve + apfst (apfst (rpair NONE)) + #> prepare_solve (fst o dest_Type oo Proof_Context.read_type_name {proper = true, strict = false}) Syntax.read_sort Syntax.read_term (singleton o Attrib.eval_thms) (fn n => replicate n (fn {context = ctxt, prems = _} => rtac ctxt UNIV_I 1));