tidied
authorpaulson
Wed Mar 03 11:12:29 1999 +0100 (1999-03-03)
changeset 63003815b5b095cb
parent 6299 1a88db6e7c7e
child 6301 08245f5a436d
tidied
src/HOL/Induct/Com.ML
     1.1 --- a/src/HOL/Induct/Com.ML	Wed Mar 03 10:50:42 1999 +0100
     1.2 +++ b/src/HOL/Induct/Com.ML	Wed Mar 03 11:12:29 1999 +0100
     1.3 @@ -38,9 +38,6 @@
     1.4  by (Blast_tac 3);
     1.5  by (Blast_tac 1);
     1.6  by (rewrite_goals_tac [Function_def, Unique_def]);
     1.7 -by (thin_tac "(?c,s1) -[ev]-> s2" 5);
     1.8 -by (rotate_tac 1 5);   (*PATCH to avoid very slow proof*)
     1.9 -(*SLOW (23s) due to proof reconstruction; needs 60s if thin_tac is omitted*)
    1.10  by (REPEAT (blast_tac (claset() addEs [exec_WHILE_case]) 1));
    1.11  qed "Function_exec";
    1.12