diff -r 5c5c1208a3fa -r 14de4d05d275 src/FOL/ex/Prolog.thy
--- a/src/FOL/ex/Prolog.thy	Wed Jun 07 16:55:39 2006 +0200
+++ b/src/FOL/ex/Prolog.thy	Wed Jun 07 23:21:55 2006 +0200
@@ -23,6 +23,66 @@
   revNil:  "rev(Nil,Nil)"
   revCons: "[| rev(xs,ys);  app(ys, x:Nil, zs) |] ==> rev(x:xs, zs)"
 
-ML {* use_legacy_bindings (the_context ()) *}
+lemma "app(a:b:c:Nil, d:e:Nil, ?x)"
+apply (rule appNil appCons)
+apply (rule appNil appCons)
+apply (rule appNil appCons)
+apply (rule appNil appCons)
+done
+
+lemma "app(?x, c:d:Nil, a:b:c:d:Nil)"
+apply (rule appNil appCons)+
+done
+
+lemma "app(?x, ?y, a:b:c:d:Nil)"
+apply (rule appNil appCons)+
+back
+back
+back
+back
+done
+
+(*app([x1,...,xn], y, ?z) requires (n+1) inferences*)
+(*rev([x1,...,xn], ?y) requires (n+1)(n+2)/2 inferences*)
+
+lemmas rules = appNil appCons revNil revCons
+
+lemma "rev(a:b:c:d:Nil, ?x)"
+apply (rule rules)+
+done
+
+lemma "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)"
+apply (rule rules)+
+done
+
+lemma "rev(?x, a:b:c:Nil)"
+apply (rule rules)+  -- {* does not solve it directly! *}
+back
+back
+done
+
+(*backtracking version*)
+ML {*
+val prolog_tac = DEPTH_FIRST (has_fewer_prems 1) (resolve_tac (thms "rules") 1)
+*}
+
+lemma "rev(?x, a:b:c:Nil)"
+apply (tactic prolog_tac)
+done
+
+lemma "rev(a:?x:c:?y:Nil, d:?z:b:?u)"
+apply (tactic prolog_tac)
+done
+
+(*rev([a..p], ?w) requires 153 inferences *)
+lemma "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil, ?w)"
+apply (tactic {* DEPTH_SOLVE (resolve_tac ([refl, conjI] @ thms "rules") 1) *})
+done
+
+(*?x has 16, ?y has 32;  rev(?y,?w) requires 561 (rather large) inferences
+  total inferences = 2 + 1 + 17 + 561 = 581*)
+lemma "a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil = ?x & app(?x,?x,?y) & rev(?y,?w)"
+apply (tactic {* DEPTH_SOLVE (resolve_tac ([refl, conjI] @ thms "rules") 1) *})
+done
 
 end