equal
deleted
inserted
replaced
66 \ move A (@x. move A x (f s) a (f t)) (f s) a (f t)"; |
66 \ move A (@x. move A x (f s) a (f t)) (f s) a (f t)"; |
67 |
67 |
68 by (subgoal_tac "? ex. move A ex (f s) a (f t)" 1); |
68 by (subgoal_tac "? ex. move A ex (f s) a (f t)" 1); |
69 by (Asm_full_simp_tac 2); |
69 by (Asm_full_simp_tac 2); |
70 by (etac exE 1); |
70 by (etac exE 1); |
71 by (rtac selectI 1); |
71 by (rtac someI 1); |
72 by (assume_tac 1); |
72 by (assume_tac 1); |
73 qed"move_is_move"; |
73 qed"move_is_move"; |
74 |
74 |
75 Goal |
75 Goal |
76 "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\ |
76 "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\ |