equal
deleted
inserted
replaced
997 by (subgoal_tac "sigma |= []<><~( (n`,$n) : #less_than )>_n" 1); |
997 by (subgoal_tac "sigma |= []<><~( (n`,$n) : #less_than )>_n" 1); |
998 by (etac thin_rl 1); |
998 by (etac thin_rl 1); |
999 by (etac STL4E 1); |
999 by (etac STL4E 1); |
1000 by (rtac DmdImpl 1); |
1000 by (rtac DmdImpl 1); |
1001 by (clarsimp_tac (temp_css addsimps2 [angle_def]) 1); |
1001 by (clarsimp_tac (temp_css addsimps2 [angle_def]) 1); |
1002 by (rtac nat_less_cases 1); |
|
1003 by Auto_tac; |
|
1004 by (rtac (temp_use wf_box_dmd_decrease) 1); |
1002 by (rtac (temp_use wf_box_dmd_decrease) 1); |
1005 by (auto_tac (temp_css addSEs2 [STL4E,DmdImplE])); |
1003 by (auto_tac (temp_css addSEs2 [STL4E,DmdImplE])); |
1006 qed "nat_box_dmd_decrease"; |
1004 qed "nat_box_dmd_decrease"; |
1007 |
1005 |
1008 |
1006 |