unused;
authorwenzelm
Sat Feb 01 18:07:10 2014 +0100 (2014-02-01)
changeset 55231264d34c19bf2
parent 55230 cb5ef74b32f9
child 55232 7a46672934a3
unused;
src/Sequents/ILL.thy
     1.1 --- a/src/Sequents/ILL.thy	Sat Feb 01 18:05:03 2014 +0100
     1.2 +++ b/src/Sequents/ILL.thy	Sat Feb 01 18:07:10 2014 +0100
     1.3 @@ -135,9 +135,6 @@
     1.4        derelict weaken promote1 promote2
     1.5        context1 context4a context4b}
     1.6      |> Cla.get_pack;
     1.7 -  
     1.8 -  fun promote_tac i =
     1.9 -    REPEAT (resolve_tac @{thms promote0 promote1 promote2} i);
    1.10  *}
    1.11  
    1.12  method_setup best_lazy = {*