equal
deleted
inserted
replaced
35 by (rtac impI 1); |
35 by (rtac impI 1); |
36 by (etac exec.induct 1); |
36 by (etac exec.induct 1); |
37 by (Blast_tac 3); |
37 by (Blast_tac 3); |
38 by (Blast_tac 1); |
38 by (Blast_tac 1); |
39 by (rewrite_goals_tac [Function_def, Unique_def]); |
39 by (rewrite_goals_tac [Function_def, Unique_def]); |
40 (*Takes ONE MINUTE due to slow proof reconstruction*) |
40 by (thin_tac "(?c,s1) -[ev]-> s2" 5); |
41 by (ALLGOALS (blast_tac (!claset addEs [exec_WHILE_case]))); |
41 (*SLOW (23s) due to proof reconstruction; needs 60s if thin_tac is omitted*) |
|
42 by (REPEAT (blast_tac (!claset addEs [exec_WHILE_case]) 1)); |
42 qed "Function_exec"; |
43 qed "Function_exec"; |
43 |
|