eliminated hard tabs;
authorwenzelm
Fri Jan 07 23:30:29 2011 +0100 (2011-01-07)
changeset 414573bb2f035203f
parent 41456 006d85ad56d3
child 41466 73981e95b30b
eliminated hard tabs;
lib/scripts/unsymbolize
src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy
     1.1 --- a/lib/scripts/unsymbolize	Fri Jan 07 23:10:33 2011 +0100
     1.2 +++ b/lib/scripts/unsymbolize	Fri Jan 07 23:30:29 2011 +0100
     1.3 @@ -46,13 +46,13 @@
     1.4      my $result = $_;
     1.5  
     1.6      if ($text ne $result) {
     1.7 -	print STDERR "fixing $file\n";
     1.8 +        print STDERR "fixing $file\n";
     1.9          if (! -f "$file~~") {
    1.10 -	    rename $file, "$file~~" || die $!;
    1.11 +            rename $file, "$file~~" || die $!;
    1.12          }
    1.13 -	open (FILE, "> $file") || die $!;
    1.14 -	print FILE $result;
    1.15 -	close FILE || die $!;
    1.16 +        open (FILE, "> $file") || die $!;
    1.17 +        print FILE $result;
    1.18 +        close FILE || die $!;
    1.19      }
    1.20  }
    1.21  
     2.1 --- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Fri Jan 07 23:10:33 2011 +0100
     2.2 +++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Fri Jan 07 23:30:29 2011 +0100
     2.3 @@ -53,7 +53,7 @@
     2.4  text {*
     2.5  qdelete(A, [A|L], L).
     2.6  qdelete(X, [A|Z], [A|R]) :-
     2.7 -	qdelete(X, Z, R).
     2.8 +  qdelete(X, Z, R).
     2.9  *}
    2.10  
    2.11  inductive qdelete :: "int => int list => int list => bool"
    2.12 @@ -64,9 +64,9 @@
    2.13  text {*
    2.14  qperm([], []).
    2.15  qperm([X|Y], K) :-
    2.16 -	qdelete(U, [X|Y], Z),
    2.17 -	K = [U|V],
    2.18 -	qperm(Z, V).
    2.19 +  qdelete(U, [X|Y], Z),
    2.20 +  K = [U|V],
    2.21 +  qperm(Z, V).
    2.22  *}
    2.23  
    2.24  inductive qperm :: "int list => int list => bool"
    2.25 @@ -77,8 +77,8 @@
    2.26  text {*
    2.27  safe([]).
    2.28  safe([N|L]) :-
    2.29 -	nodiag(N, 1, L),
    2.30 -	safe(L).
    2.31 +  nodiag(N, 1, L),
    2.32 +  safe(L).
    2.33  *}
    2.34  
    2.35  inductive safe :: "int list => bool"
    2.36 @@ -88,8 +88,8 @@
    2.37  
    2.38  text {*
    2.39  queen(Data, Out) :-
    2.40 -	qperm(Data, Out),
    2.41 -	safe(Out)
    2.42 +  qperm(Data, Out),
    2.43 +  safe(Out)
    2.44  *}
    2.45  
    2.46  inductive queen :: "int list => int list => bool"
    2.47 @@ -113,36 +113,36 @@
    2.48  text {*
    2.49  
    2.50  d(U + V, X, DU + DV) :-
    2.51 -	cut,
    2.52 -	d(U, X, DU),
    2.53 -	d(V, X, DV).
    2.54 +  cut,
    2.55 +  d(U, X, DU),
    2.56 +  d(V, X, DV).
    2.57  d(U - V, X, DU - DV) :-
    2.58 -	cut,
    2.59 -	d(U, X, DU),
    2.60 -	d(V, X, DV).
    2.61 +  cut,
    2.62 +  d(U, X, DU),
    2.63 +  d(V, X, DV).
    2.64  d(U * V, X, DU * V + U * DV) :-
    2.65 -	cut,
    2.66 -	d(U, X, DU),
    2.67 -	d(V, X, DV).
    2.68 +  cut,
    2.69 +  d(U, X, DU),
    2.70 +  d(V, X, DV).
    2.71  d(U / V, X, (DU * V - U * DV) / ^(V, 2)) :-
    2.72 -	cut,
    2.73 -	d(U, X, DU),
    2.74 -	d(V, X, DV).
    2.75 +  cut,
    2.76 +  d(U, X, DU),
    2.77 +  d(V, X, DV).
    2.78  d(^(U, N), X, DU * num(N) * ^(U, N1)) :-
    2.79 -	cut,
    2.80 -	N1 is N - 1,
    2.81 -	d(U, X, DU).
    2.82 +  cut,
    2.83 +  N1 is N - 1,
    2.84 +  d(U, X, DU).
    2.85  d(-U, X, -DU) :-
    2.86 -	cut,
    2.87 -	d(U, X, DU).
    2.88 +  cut,
    2.89 +  d(U, X, DU).
    2.90  d(exp(U), X, exp(U) * DU) :-
    2.91 -	cut,
    2.92 -	d(U, X, DU).
    2.93 +  cut,
    2.94 +  d(U, X, DU).
    2.95  d(log(U), X, DU / U) :-
    2.96 -	cut,
    2.97 -	d(U, X, DU).
    2.98 +  cut,
    2.99 +  d(U, X, DU).
   2.100  d(x, X, num(1)) :-
   2.101 -	cut.
   2.102 +  cut.
   2.103  d(num(_), _, num(0)).
   2.104  
   2.105  *}
   2.106 @@ -162,16 +162,16 @@
   2.107  
   2.108  text {*
   2.109  ops8(E) :-
   2.110 -	d((x + num(1)) * ((^(x, 2) + num(2)) * (^(x, 3) + num(3))), x, E).
   2.111 +  d((x + num(1)) * ((^(x, 2) + num(2)) * (^(x, 3) + num(3))), x, E).
   2.112  
   2.113  divide10(E) :-
   2.114 -	d(((((((((x / x) / x) / x) / x) / x) / x) / x) / x) / x, x, E).
   2.115 +  d(((((((((x / x) / x) / x) / x) / x) / x) / x) / x) / x, x, E).
   2.116  
   2.117  log10(E) :-
   2.118 -	d(log(log(log(log(log(log(log(log(log(log(x)))))))))), x, E).
   2.119 +  d(log(log(log(log(log(log(log(log(log(log(x)))))))))), x, E).
   2.120  
   2.121  times10(E) :-
   2.122 -	d(((((((((x * x) * x) * x) * x) * x) * x) * x) * x) * x, x, E)
   2.123 +  d(((((((((x * x) * x) * x) * x) * x) * x) * x) * x) * x, x, E)
   2.124  *}
   2.125  
   2.126  inductive ops8 :: "expr => bool"