[isabelle] using global theorems in locale context
I have the following theorem
lemma small_fusion: "h : Disjunctive ==> mono f ==> mono g ==> h o f = g
o h ==> h (lfp f) = lfp g"
which is proved as a global theorem.
However I would like to use it in a context of a complete lattice
apply (cut_tac ... in small_fusion)
The main reason I have small_fusion as a global theorem is because I use
lfp_ordinal_induct to prove it. If I want to prove small_fusion in the
of a complete lattice, then I would have to build everything about lfp
in the local context.
This archive was generated by a fusion of
Pipermail (Mailman edition) and