--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Fri Jan 07 23:10:33 2011 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Fri Jan 07 23:30:29 2011 +0100
@@ -53,7 +53,7 @@
text {*
qdelete(A, [A|L], L).
qdelete(X, [A|Z], [A|R]) :-
- qdelete(X, Z, R).
+ qdelete(X, Z, R).
*}
inductive qdelete :: "int => int list => int list => bool"
@@ -64,9 +64,9 @@
text {*
qperm([], []).
qperm([X|Y], K) :-
- qdelete(U, [X|Y], Z),
- K = [U|V],
- qperm(Z, V).
+ qdelete(U, [X|Y], Z),
+ K = [U|V],
+ qperm(Z, V).
*}
inductive qperm :: "int list => int list => bool"
@@ -77,8 +77,8 @@
text {*
safe([]).
safe([N|L]) :-
- nodiag(N, 1, L),
- safe(L).
+ nodiag(N, 1, L),
+ safe(L).
*}
inductive safe :: "int list => bool"
@@ -88,8 +88,8 @@
text {*
queen(Data, Out) :-
- qperm(Data, Out),
- safe(Out)
+ qperm(Data, Out),
+ safe(Out)
*}
inductive queen :: "int list => int list => bool"
@@ -113,36 +113,36 @@
text {*
d(U + V, X, DU + DV) :-
- cut,
- d(U, X, DU),
- d(V, X, DV).
+ cut,
+ d(U, X, DU),
+ d(V, X, DV).
d(U - V, X, DU - DV) :-
- cut,
- d(U, X, DU),
- d(V, X, DV).
+ cut,
+ d(U, X, DU),
+ d(V, X, DV).
d(U * V, X, DU * V + U * DV) :-
- cut,
- d(U, X, DU),
- d(V, X, DV).
+ cut,
+ d(U, X, DU),
+ d(V, X, DV).
d(U / V, X, (DU * V - U * DV) / ^(V, 2)) :-
- cut,
- d(U, X, DU),
- d(V, X, DV).
+ cut,
+ d(U, X, DU),
+ d(V, X, DV).
d(^(U, N), X, DU * num(N) * ^(U, N1)) :-
- cut,
- N1 is N - 1,
- d(U, X, DU).
+ cut,
+ N1 is N - 1,
+ d(U, X, DU).
d(-U, X, -DU) :-
- cut,
- d(U, X, DU).
+ cut,
+ d(U, X, DU).
d(exp(U), X, exp(U) * DU) :-
- cut,
- d(U, X, DU).
+ cut,
+ d(U, X, DU).
d(log(U), X, DU / U) :-
- cut,
- d(U, X, DU).
+ cut,
+ d(U, X, DU).
d(x, X, num(1)) :-
- cut.
+ cut.
d(num(_), _, num(0)).
*}
@@ -162,16 +162,16 @@
text {*
ops8(E) :-
- d((x + num(1)) * ((^(x, 2) + num(2)) * (^(x, 3) + num(3))), x, E).
+ d((x + num(1)) * ((^(x, 2) + num(2)) * (^(x, 3) + num(3))), x, E).
divide10(E) :-
- d(((((((((x / x) / x) / x) / x) / x) / x) / x) / x) / x, x, E).
+ d(((((((((x / x) / x) / x) / x) / x) / x) / x) / x) / x, x, E).
log10(E) :-
- d(log(log(log(log(log(log(log(log(log(log(x)))))))))), x, E).
+ d(log(log(log(log(log(log(log(log(log(log(x)))))))))), x, E).
times10(E) :-
- d(((((((((x * x) * x) * x) * x) * x) * x) * x) * x) * x, x, E)
+ d(((((((((x * x) * x) * x) * x) * x) * x) * x) * x) * x, x, E)
*}
inductive ops8 :: "expr => bool"