Object: combin_simpset, theory combin
Display form: map (add_to_simpset `combin`) ( [pattern_unfold_op `compose_unfold` `compose` [(x o x@0) x@1] ;lemma_to_simp `o_assoc` ] @ lemma_simps `i_o_id` ) ;;
Term structure: map (add_to_simpset `combin`) ( [pattern_unfold_op `compose_unfold` `compose` [ apply(compose(x; x@0); x@1) ] ;lemma_to_simp `o_assoc` ] @ lemma_simps `i_o_id` ) ;;