| changeset 11701 | 3d51fbf81c17 |
| parent 9015 | 8006e9009621 |
| child 12486 | 0ed8bdd883e0 |
--- a/src/HOL/Prolog/Type.ML Fri Oct 05 21:50:37 2001 +0200 +++ b/src/HOL/Prolog/Type.ML Fri Oct 05 21:52:39 2001 +0200 @@ -6,7 +6,7 @@ pgoal "typeof (fix (%x. x)) ?T"; -pgoal "typeof (fix (%fact. abs(%n. (app fact (n-0))))) ?T"; +pgoal "typeof (fix (%fact. abs(%n. (app fact (n - 0))))) ?T"; pgoal "typeof (fix (%fact. abs(%n. cond (n eq 0) (S 0) \ \(n * (app fact (n - (S 0))))))) ?T";