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

> I was importing the one defined in theory Fact, which I got (without > defining it myself) from the line "theory Factorial imports Main Fact > begin ...": > fun > fact_nat :: "nat => nat" > where > fact__nat: "fact_nat 0 = Suc 0" > | fact-Suc: "fact_nat (Suc x) = Suc x * fact x" > I'm not sure, by the way, why this is called fact_nat in theory Fact, > rather than just fact. After digging a bit, it turns out that the Fact theory is part of HOL in Isabelle2014, but not anymore in Isabelle2015-RC*. I couldn't reproduce the tactic failure, though. 'simp add: eval_nat_numeral' solves the goal just fine. Cheers Lars

**Follow-Ups**:**Re: [isabelle] What is sumC?***From:*Larry Paulson

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

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

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

- Previous by Date: Re: [isabelle] What is sumC?
- Next by Date: [isabelle] Postdoc positions at Inria-Saclay
- 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