--- a/src/HOL/Finite_Set.thy Mon Jun 12 21:19:07 2006 +0200
+++ b/src/HOL/Finite_Set.thy Mon Jun 12 22:14:38 2006 +0200
@@ -499,10 +499,9 @@
text{* Interpretation of locales: *}
interpretation AC_add: ACe ["op +" "0::'a::comm_monoid_add"]
-by(auto intro: ACf.intro ACe_axioms.intro add_assoc add_commute)
+ by(auto intro: ACf.intro ACe_axioms.intro add_assoc add_commute)
interpretation AC_mult: ACe ["op *" "1::'a::comm_monoid_mult"]
- apply -
apply (fast intro: ACf.intro mult_assoc mult_commute)
apply (fastsimp intro: ACe_axioms.intro mult_assoc mult_commute)
done
@@ -511,7 +510,7 @@
subsubsection{*From @{term foldSet} to @{term fold}*}
lemma image_less_Suc: "h ` {i. i < Suc m} = insert (h m) (h ` {i. i < m})"
-by (auto simp add: less_Suc_eq)
+ by (auto simp add: less_Suc_eq)
lemma insert_image_inj_on_eq:
"[|insert (h m) A = h ` {i. i < Suc m}; h m \<notin> A;
--- a/src/Pure/Tools/invoke.ML Mon Jun 12 21:19:07 2006 +0200
+++ b/src/Pure/Tools/invoke.ML Mon Jun 12 22:14:38 2006 +0200
@@ -69,20 +69,16 @@
val params'' = map (Thm.term_of o Drule.dest_term) res_params;
val elems' = elems |> map (Element.inst_ctxt thy
(Symtab.make (map #1 types ~~ types''), Symtab.make (map #1 params ~~ params'')));
+ val prems'' = map2 Element.make_witness (maps Element.prems_of elems') res_prems;
- val prems'' = map2 Element.make_witness (maps Element.prems_of elems') res_prems;
val Element.Notes notes =
Element.Notes (maps (Element.facts_of thy) elems')
|> Element.satisfy_ctxt prems''
|> Element.map_ctxt_values I I (ProofContext.export ctxt'' ctxt);
- (* FIXME export typs/terms *)
-
- val _ = print notes;
-
+ (* FIXME export typs/terms *)
val notes' = notes
|> Attrib.map_facts (Attrib.attribute_i thy)
|> map (fn ((a, atts), facts) => ((a, atts @ more_atts), facts));
-
in
ctxt
|> ProofContext.sticky_prefix prfx
@@ -92,7 +88,7 @@
end) #> Proof.put_facts NONE);
in
state'
- |> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_schematic_i
+ |> Proof.local_goal (K (K ())) (K I) ProofContext.bind_propp_schematic_i
"invoke" NONE after_qed propp
|> Element.refine_witness
|> Seq.hd