*To*: M A <tesleft at hotmail.com>, "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Failed to parse term*From*: Buday Gergely <gbuday at karolyrobert.hu>*Date*: Wed, 29 Oct 2014 13:28:46 +0100*Accept-language*: en-US, hu-HU*Acceptlanguage*: en-US, hu-HU*In-reply-to*: <BAY167-W10078F5DD087F07D31EA9C1B69C0@phx.gbl>*References*: <BAY167-W3024082D992B681F64185DB69E0@phx.gbl>, , <BAY167-W27953B618A80B2575F3851B69E0@phx.gbl>, , , , <16FFFE45-32C8-44B9-8908-A9471D2F4C7D@uibk.ac.at>, , <BAY167-W1074477050F04D10DA461BBB69E0@phx.gbl>, , <alpine.LNX.2.00.1410272003580.59545@lxbroy10.informatik.tu-muenchen.de>, <BAY167-W1086A25A3C2791880694439B69E0@phx.gbl>, <BAY167-W107C4A117B19EE941F4B91DB69C0@phx.gbl> <BAY167-W10078F5DD087F07D31EA9C1B69C0@phx.gbl>*Thread-index*: Ac/zbuRPtyOicvf6SFiKADHtpogBRAABLp5Q*Thread-topic*: [isabelle] Failed to parse term

Hi Martin, what is your definition of @ ? Did you get it from the Tutorial? As I mentioned it would be better to provide us a working Isabelle theory containing theory Blabla imports main and all the necessary definitions so we could try it out. - Gergely -----Original Message----- From: cl-isabelle-users-bounces at lists.cam.ac.uk [mailto:cl-isabelle-users-bounces at lists.cam.ac.uk] On Behalf Of M A Sent: Wednesday, October 29, 2014 12:42 PM To: isabelle-users at cl.cam.ac.uk Subject: [isabelle] Failed to parse term Hi i am a beginner, first time to write primrec from lemma, however got an error when parse. lemma map_app [simp]: "map f xs @ map f ys = map f (xs @ ys)" apply(induct_tac xs) apply(auto) done goal (2 subgoals): 1. map f [] @ map f ys = map f ([] @ ys) 2. ⋀a list. map f list @ map f ys = map f (list @ ys) ⟹ map f (a # list) @ map f ys = map f ((a # list) @ ys) prepare to edit primrev map f [] = [] map f (a # list) @ map f ys = map f ((a # list) @ ys) final resultprimrec mmap :: "'a => 'a => 'a list => 'a list" where "mmap f [] = []" | "mmap f ((mmap f x) # (mmap f xs)) = mmap f (x # xs)" value "mmap x+1 [1, 2]" Inner syntax error⌂ Failed to parse term Regards, Martin

**References**:**[isabelle] is it possible to find the function from lemmas and which command can do?***From:*M A

**[isabelle] how to type logical and and logical or operators in Isabelle***From:*M A

**[isabelle] where is "Isabelle/Show me .../Facts" menu in window version of Isabelle***From:*M A

**Re: [isabelle] where is "Isabelle/Show me .../Facts" menu in window version of Isabelle***From:*Makarius

**Re: [isabelle] where is "Isabelle/Show me .../Facts" menu in window version of Isabelle***From:*M A

**[isabelle] Failed to parse term after convert to primrec***From:*M A

**[isabelle] Failed to parse term***From:*M A

- Previous by Date: Re: [isabelle] how to use brackets in lemma
- Next by Date: Re: [isabelle] Isabelle2014-RC2: PIDE does not resume processing
- Previous by Thread: [isabelle] Failed to parse term
- Next by Thread: Re: [isabelle] Failed to parse term
- Cl-isabelle-users October 2014 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