src/HOL/Prolog/Func.thy
changeset 36319 8feb2c4bef1a
parent 35301 90e42f9ba4d1
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Prolog/Func.thy	Fri Apr 23 23:33:48 2010 +0200
     1.2 +++ b/src/HOL/Prolog/Func.thy	Fri Apr 23 23:35:43 2010 +0200
     1.3 @@ -58,11 +58,11 @@
     1.4  
     1.5  lemmas prog_Func = eval
     1.6  
     1.7 -lemma "eval ((S (S Z)) + (S Z)) ?X"
     1.8 +schematic_lemma "eval ((S (S Z)) + (S Z)) ?X"
     1.9    apply (prolog prog_Func)
    1.10    done
    1.11  
    1.12 -lemma "eval (app (fix (%fact. abs(%n. cond (n eq Z) (S Z)
    1.13 +schematic_lemma "eval (app (fix (%fact. abs(%n. cond (n eq Z) (S Z)
    1.14                          (n * (app fact (n - (S Z))))))) (S (S (S Z)))) ?X"
    1.15    apply (prolog prog_Func)
    1.16    done