--- a/src/HOL/Prolog/Test.ML Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/Prolog/Test.ML Thu Dec 13 15:45:03 2001 +0100
@@ -1,7 +1,7 @@
open Test;
val prog_Test = prog_HOHH@[append, reverse, mappred, mapfun, age, eq, bag_appl];
-fun pgoal s = (case Goal s of _ => by(prolog_tac prog_Test));
+fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Test));
val p = ptac prog_Test 1;
pgoal "append ?x ?y [a,b,c,d]";
@@ -40,8 +40,8 @@
(*
goal thy "f a = ?g a a & ?g = x";
-by(rtac conjI 1);
-by(rtac refl 1);
+by (rtac conjI 1);
+by (rtac refl 1);
back();
back();
*)
@@ -103,19 +103,19 @@
(* implication and disjunction in atom: *)
goal thy "? Q. (!p q. R(q :- p) => R(Q p q)) & Q (t | s) (s | t)";
-by(fast_tac HOL_cs 1);
+by (fast_tac HOL_cs 1);
(* disjunction in atom: *)
goal thy "(!P. g P :- (P => b | a)) => g(a | b)";
-by(step_tac HOL_cs 1);
-by(step_tac HOL_cs 1);
-by(step_tac HOL_cs 1);
-by(fast_tac HOL_cs 2);
-by(fast_tac HOL_cs 1);
+by (step_tac HOL_cs 1);
+by (step_tac HOL_cs 1);
+by (step_tac HOL_cs 1);
+by (fast_tac HOL_cs 2);
+by (fast_tac HOL_cs 1);
(*
hangs:
goal thy "(!P. g P :- (P => b | a)) => g(a | b)";
-by(fast_tac HOL_cs 1);
+by (fast_tac HOL_cs 1);
*)
pgoal "!Emp Stk.(\