[isabelle] Failed to parse term after convert to primrec



Hi
in quickspec, i find a lemma and then get 2 subgoals, after rewrite subgoals as primrec and value to see how it works.it return failed to parse term, how to write it and parse successfully?
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 editprimrevmap 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.