equal
deleted
inserted
replaced
405 declare list_all2_Nil [code] |
405 declare list_all2_Nil [code] |
406 declare list_all2_Cons [code] |
406 declare list_all2_Cons [code] |
407 |
407 |
408 lemma xcpt_app_lemma [code]: |
408 lemma xcpt_app_lemma [code]: |
409 "xcpt_app i G pc et = list_all (is_class G) (xcpt_names (i, G, pc, et))" |
409 "xcpt_app i G pc et = list_all (is_class G) (xcpt_names (i, G, pc, et))" |
410 by (simp add: list_all_conv) |
410 by (simp add: list_all_iff) |
411 |
411 |
412 lemmas [simp del] = app_def xcpt_app_def |
412 lemmas [simp del] = app_def xcpt_app_def |
413 |
413 |
414 end |
414 end |