src/HOL/Prolog/Func.thy
changeset 61337 4645502c3c64
parent 58889 5b7a9633cfa8
child 63167 0909deb8059b
     1.1 --- a/src/HOL/Prolog/Func.thy	Tue Oct 06 13:31:44 2015 +0200
     1.2 +++ b/src/HOL/Prolog/Func.thy	Tue Oct 06 15:14:28 2015 +0200
     1.3 @@ -58,11 +58,11 @@
     1.4  
     1.5  lemmas prog_Func = eval
     1.6  
     1.7 -schematic_lemma "eval ((S (S Z)) + (S Z)) ?X"
     1.8 +schematic_goal "eval ((S (S Z)) + (S Z)) ?X"
     1.9    apply (prolog prog_Func)
    1.10    done
    1.11  
    1.12 -schematic_lemma "eval (app (fix (%fact. abs(%n. cond (n eq Z) (S Z)
    1.13 +schematic_goal "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