In Analysis, we have two equivalent definitions of continuous functions between 
two topological spaces:

lemma "continuous_map X Y f = continuous_on_topo X Y f"
  by (auto simp add: continuous_map_def continuous_on_topo_def vimage_def 
image_def Collect_conj_eq inf_commute)

The first one comes from HOL Light and is defined in Abstract_Topology. The 
latter is declared in Function_Topology.

Obviously we need to eliminate one of them, and I prefer the former name. The 
latter is more logical but clunky, especially when compound with others in 
theorem names.

Any comments?


isabelle-dev mailing list

Reply via email to