--- a/src/HOL/Prolog/Type.thy Tue Oct 06 13:31:44 2015 +0200
+++ b/src/HOL/Prolog/Type.thy Tue Oct 06 15:14:28 2015 +0200
@@ -46,41 +46,41 @@
lemmas prog_Type = prog_Func good_typeof common_typeof
-schematic_lemma "typeof (abs(%n. abs(%m. abs(%p. p and (n eq m))))) ?T"
+schematic_goal "typeof (abs(%n. abs(%m. abs(%p. p and (n eq m))))) ?T"
apply (prolog prog_Type)
done
-schematic_lemma "typeof (fix (%x. x)) ?T"
+schematic_goal "typeof (fix (%x. x)) ?T"
apply (prolog prog_Type)
done
-schematic_lemma "typeof (fix (%fact. abs(%n. (app fact (n - Z))))) ?T"
+schematic_goal "typeof (fix (%fact. abs(%n. (app fact (n - Z))))) ?T"
apply (prolog prog_Type)
done
-schematic_lemma "typeof (fix (%fact. abs(%n. cond (n eq Z) (S Z)
+schematic_goal "typeof (fix (%fact. abs(%n. cond (n eq Z) (S Z)
(n * (app fact (n - (S Z))))))) ?T"
apply (prolog prog_Type)
done
-schematic_lemma "typeof (abs(%v. Z)) ?T" (*correct only solution (?A1 -> nat) *)
+schematic_goal "typeof (abs(%v. Z)) ?T" (*correct only solution (?A1 -> nat) *)
apply (prolog prog_Type)
done
-schematic_lemma "typeof (abs(%v. Z)) ?T"
+schematic_goal "typeof (abs(%v. Z)) ?T"
apply (prolog bad1_typeof common_typeof) (* 1st result ok*)
done
-schematic_lemma "typeof (abs(%v. Z)) ?T"
+schematic_goal "typeof (abs(%v. Z)) ?T"
apply (prolog bad1_typeof common_typeof)
back (* 2nd result (?A1 -> ?A1) wrong *)
done
-schematic_lemma "typeof (abs(%v. abs(%v. app v v))) ?T"
+schematic_goal "typeof (abs(%v. abs(%v. app v v))) ?T"
apply (prolog prog_Type)? (*correctly fails*)
oops
-schematic_lemma "typeof (abs(%v. abs(%v. app v v))) ?T"
+schematic_goal "typeof (abs(%v. abs(%v. app v v))) ?T"
apply (prolog bad2_typeof common_typeof) (* wrong result ((?A3 -> ?B3) -> ?A3 -> ?B3)*)
done