[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 		 	   		   		 	   		  


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.