equal
deleted
inserted
replaced
351 apply (unfold externals_def actions_def compatible_def) |
351 apply (unfold externals_def actions_def compatible_def) |
352 apply simp |
352 apply simp |
353 apply blast |
353 apply blast |
354 done |
354 done |
355 |
355 |
356 lemmas ext1_ext2_is_not_act2 = ext1_is_not_int2 [THEN int_and_ext_is_act, standard] |
356 lemmas ext1_ext2_is_not_act2 = ext1_is_not_int2 [THEN int_and_ext_is_act] |
357 lemmas ext1_ext2_is_not_act1 = ext2_is_not_int1 [THEN int_and_ext_is_act, standard] |
357 lemmas ext1_ext2_is_not_act1 = ext2_is_not_int1 [THEN int_and_ext_is_act] |
358 |
358 |
359 lemma intA_is_not_extB: |
359 lemma intA_is_not_extB: |
360 "[| compatible A B; x:int A |] ==> x~:ext B" |
360 "[| compatible A B; x:int A |] ==> x~:ext B" |
361 apply (unfold externals_def actions_def compatible_def) |
361 apply (unfold externals_def actions_def compatible_def) |
362 apply simp |
362 apply simp |