equal
deleted
inserted
replaced
534 done |
534 done |
535 |
535 |
536 ML {* bind_thms ("ask_inv_client_map_drop_map'", make_o_equivs @{thm ask_inv_client_map_drop_map}) *} |
536 ML {* bind_thms ("ask_inv_client_map_drop_map'", make_o_equivs @{thm ask_inv_client_map_drop_map}) *} |
537 declare ask_inv_client_map_drop_map [simp] |
537 declare ask_inv_client_map_drop_map [simp] |
538 |
538 |
539 |
|
540 declare finite_lessThan [iff] |
|
541 |
539 |
542 text{*Client : <unfolded specification> *} |
540 text{*Client : <unfolded specification> *} |
543 lemmas client_spec_simps = |
541 lemmas client_spec_simps = |
544 client_spec_def client_increasing_def client_bounded_def |
542 client_spec_def client_increasing_def client_bounded_def |
545 client_progress_def client_allowed_acts_def client_preserves_def |
543 client_progress_def client_allowed_acts_def client_preserves_def |