new backchain requires explicit bounds

This is probably a bug that should be fixed
abella-prover · Oct 14, 2016 · 8e89512 · 8e89512
1 parent 68771ed
commit 8e89512
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/examples/process-calculi/ccs/ccs_bisim.thm b/examples/process-calculi/ccs/ccs_bisim.thm
@@ -33,7 +33,7 @@ unfold.
     Link : apply bisim_transitive_ to Left3 Bisim.
     Link : apply bisim_symmetric_ to Bisim1.
     Link : apply bisim_transitive_ to Link1 Right3.
-    backchain CH.
+    backchain 1 CH.
 
   intros Qstep.
     Right : case Right. Right : apply Right1 to Qstep. clear Right Right1. rename Right2 to Pstep.
@@ -46,7 +46,7 @@ unfold.
     Link : apply bisim_transitive_ to Left4 Link.
     Link : apply bisim_symmetric_ to Link1.
     Link : apply bisim_transitive_ to Link3 Right4.
-    backchain CH.
+    backchain 1 CH.
 
 Theorem bisim_sound_snd : is_sound_snd bisim_t.
 unfold. intros.