src/HOL/Bali/Table.thy
changeset 18447 da548623916a
parent 16417 9bc16273c2d4
child 24038 18182c4aec9e
     1.1 --- a/src/HOL/Bali/Table.thy	Tue Dec 20 22:06:00 2005 +0100
     1.2 +++ b/src/HOL/Bali/Table.thy	Wed Dec 21 12:02:57 2005 +0100
     1.3 @@ -206,10 +206,7 @@
     1.4  
     1.5  lemma set_get_eq: 
     1.6    "unique l \<Longrightarrow> (k, the (table_of l k)) \<in> set l = (table_of l k \<noteq> None)"
     1.7 -apply safe
     1.8 -apply (fast dest!: weak_map_of_SomeI)
     1.9 -apply auto
    1.10 -done
    1.11 +by (auto dest!: weak_map_of_SomeI)
    1.12  
    1.13  lemma inj_Pair_const2: "inj (\<lambda>k. (k, C))"
    1.14  apply (rule inj_onI)