changeset 26306 | ed3375ac152d |
parent 25135 | 4f8176c940cf |
child 26359 | 6d437bde2f1d |
--- a/src/HOLCF/IOA/meta_theory/RefMappings.thy Mon Mar 17 18:37:07 2008 +0100 +++ b/src/HOLCF/IOA/meta_theory/RefMappings.thy Mon Mar 17 18:37:08 2008 +0100 @@ -69,7 +69,7 @@ subsection "weak_ref_map and ref_map" -lemma imp_conj_lemma: +lemma weak_ref_map2ref_map: "[| ext C = ext A; is_weak_ref_map f C A |] ==> is_ref_map f C A" apply (unfold is_weak_ref_map_def is_ref_map_def)