# HG changeset patch # User blanchet # Date 1409581066 -7200 # Node ID 1c8541513acbfad08df28bccf72411cb67210ad8 # Parent f3c5360711e96ff7461b5364821cb8b63d041d1c tuned whitespace diff -r f3c5360711e9 -r 1c8541513acb src/HOL/Tools/BNF/bnf_def.ML --- a/src/HOL/Tools/BNF/bnf_def.ML Mon Sep 01 13:53:39 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_def.ML Mon Sep 01 16:17:46 2014 +0200 @@ -1045,8 +1045,7 @@ end; fun mk_map_cong_prem mk_implies x z set f f_copy = - Logic.all z (mk_implies - (mk_Trueprop_mem (z, set $ x), mk_Trueprop_eq (f $ z, f_copy $ z))); + Logic.all z (mk_implies (mk_Trueprop_mem (z, set $ x), mk_Trueprop_eq (f $ z, f_copy $ z))); val map_cong0_goal = let @@ -1061,8 +1060,7 @@ let fun mk_goal setA setB f = let - val set_comp_map = - HOLogic.mk_comp (setB, Term.list_comb (bnf_map_AsBs, fs)); + val set_comp_map = HOLogic.mk_comp (setB, Term.list_comb (bnf_map_AsBs, fs)); val image_comp_set = HOLogic.mk_comp (mk_image f, setA); in fold_rev Logic.all fs (mk_Trueprop_eq (set_comp_map, image_comp_set)) @@ -1105,11 +1103,9 @@ val z = nth zs i; val set_wit = nth bnf_sets_As i $ Term.list_comb (wit, xs); val concl = HOLogic.mk_Trueprop - (if member (op =) I i then HOLogic.mk_eq (z, nth bs i) - else @{term False}); + (if member (op =) I i then HOLogic.mk_eq (z, nth bs i) else @{term False}); in - fold_rev Logic.all (z :: xs) - (Logic.mk_implies (mk_Trueprop_mem (z, set_wit), concl)) + fold_rev Logic.all (z :: xs) (Logic.mk_implies (mk_Trueprop_mem (z, set_wit), concl)) end; in map wit_goal (0 upto live - 1) @@ -1131,12 +1127,10 @@ fun mk_collect_set_map () = let val defT = mk_bnf_T Ts Calpha --> HOLogic.mk_setT T; - val collect_map = HOLogic.mk_comp - (mk_collect (map (mk_bnf_t Ts) bnf_sets) defT, + val collect_map = HOLogic.mk_comp (mk_collect (map (mk_bnf_t Ts) bnf_sets) defT, Term.list_comb (mk_bnf_map As' Ts, hs)); val image_collect = mk_collect - (map2 (fn h => fn set => HOLogic.mk_comp (mk_image h, set)) hs bnf_sets_As) - defT; + (map2 (fn h => fn set => HOLogic.mk_comp (mk_image h, set)) hs bnf_sets_As) defT; (*collect {set1 ... setm} o map f1 ... fm = collect {f1` o set1 ... fm` o setm}*) val goal = fold_rev Logic.all hs (mk_Trueprop_eq (collect_map, image_collect)); in