changeset 171 | 16c4ea954511 |
parent 168 | 44ff2275d44f |
child 224 | 060ea04f6b50 |
--- a/IOA/example/Correctness.ML Fri Nov 11 10:35:03 1994 +0100 +++ b/IOA/example/Correctness.ML Mon Nov 21 17:50:34 1994 +0100 @@ -42,7 +42,7 @@ by(Action.action.induct_tac "a" 1); by(ALLGOALS(simp_tac (action_ss addsimps (actions_def :: asig_projections @ set_lemmas)))); -val externals_lemma = result(); +qed "externals_lemma"; val sels = [Sender.sbit_def, Sender.sq_def, Sender.ssending_def,