*To*: "W. Douglas Maurer" <maurer at gwu.edu>*Subject*: Re: [isabelle] What is sumC?*From*: Lars Hupel <hupel at in.tum.de>*Date*: Sun, 26 Apr 2015 09:07:12 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <a06200718d161f76ac66e@[192.168.1.6]>*References*: <a06200714d16044799025@[192.168.1.6]> <553B503D.2050200@in.tum.de> <a06200718d161f76ac66e@[192.168.1.6]>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.6.0

> That doesn't work. When I type in: > lemma "fact 3 = 6" unfolding eval_nat_numeral BitM.simps by simp > I get the message: > Failed to apply initial proof method: goal (1 subgoal): 1. fact 3 = 6 Can you give the definition of your 'fact' function? I was assuming something along those lines: fun fact :: "nat => nat" where "fact 0 = 1" | "fact (Suc n) = (Suc n) * fact n"

**References**:**[isabelle] What is sumC?***From:*W. Douglas Maurer

**Re: [isabelle] What is sumC?***From:*Lars Hupel

- Previous by Date: Re: [isabelle] What is sumC?
- Next by Date: Re: [isabelle] What is sumC?
- Previous by Thread: Re: [isabelle] What is sumC?
- Next by Thread: Re: [isabelle] What is sumC?
- Cl-isabelle-users April 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list