author | paulson |
Fri, 12 Dec 1997 10:32:45 +0100 | |
changeset 4390 | 57e16404c2a9 |
parent 4389 | 1865cb8df116 |
child 4391 | cc3e8453d7f0 |
--- a/src/HOL/Induct/Com.ML Fri Dec 12 10:31:25 1997 +0100 +++ b/src/HOL/Induct/Com.ML Fri Dec 12 10:32:45 1997 +0100 @@ -38,6 +38,7 @@ by (Blast_tac 1); by (rewrite_goals_tac [Function_def, Unique_def]); by (thin_tac "(?c,s1) -[ev]-> s2" 5); +by (rotate_tac 1 5); (*PATCH to avoid very slow proof*) (*SLOW (23s) due to proof reconstruction; needs 60s if thin_tac is omitted*) by (REPEAT (blast_tac (claset() addEs [exec_WHILE_case]) 1)); qed "Function_exec";