Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Prolog/Type.ML
changeset 20713 823967ef47f1
parent 14981 e73f8140af78 
--- a/src/HOL/Prolog/Type.ML	Tue Sep 26 13:34:15 2006 +0200
+++ b/src/HOL/Prolog/Type.ML	Tue Sep 26 13:34:16 2006 +0200
@@ -11,13 +11,13 @@
 
 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 - Z))))) ?T";
 
-pgoal "typeof (fix (%fact. abs(%n. cond (n eq 0) (S 0) \
-				\(n * (app fact (n - (S 0))))))) ?T";
+pgoal "typeof (fix (%fact. abs(%n. cond (n eq Z) (S Z) \
+  \(n * (app fact (n - (S Z))))))) ?T";
 
-pgoal "typeof (abs(%v. 0)) ?T"; (*correct only solution (?A1 -> nat) *)
-Goal "typeof (abs(%v. 0)) ?T";
+pgoal "typeof (abs(%v. Z)) ?T"; (*correct only solution (?A1 -> nat) *)
+Goal "typeof (abs(%v. Z)) ?T";
 by (prolog_tac [bad1_typeof,common_typeof]); (* 1st result ok*)
 back(); (* 2nd result (?A1 -> ?A1) wrong *)
isabelle