src/HOL/Induct/Com.ML
changeset 4390 57e16404c2a9
parent 4089 96fba19bcbe2
child 4686 74a12e86b20b
equal deleted inserted replaced
4389:1865cb8df116 4390:57e16404c2a9
    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 by (thin_tac "(?c,s1) -[ev]-> s2" 5);
    40 by (thin_tac "(?c,s1) -[ev]-> s2" 5);
       
    41 by (rotate_tac 1 5);   (*PATCH to avoid very slow proof*)
    41 (*SLOW (23s) due to proof reconstruction; needs 60s if thin_tac is omitted*)
    42 (*SLOW (23s) due to proof reconstruction; needs 60s if thin_tac is omitted*)
    42 by (REPEAT (blast_tac (claset() addEs [exec_WHILE_case]) 1));
    43 by (REPEAT (blast_tac (claset() addEs [exec_WHILE_case]) 1));
    43 qed "Function_exec";
    44 qed "Function_exec";
    44 
    45 
    45 
    46