Re: [isabelle] Record simplification



Hello Benny,

On Wednesday 28 December 2005 15:47, shimonyb at techunix.technion.ac.il wrote:
> types 'a edge = "'a set"
>
> record 'a pre_graph =
>   Verts :: "'a set"
>   Edges :: "'a edge set"
> types ('a,'b) forest = "('a,'b) pre_graph_scheme set"
>
> constdefs start_forest :: "('a, 'b) pre_graph_scheme ==> ('a,'b) forest"
>  "start_forest H == { (|Verts={v},Edges={} |) | v.   v: (Verts H)  }"

Your declaration of start_forest is to general. You definition only defines
"start_forest:: 'a pre_graph => 'a pre_graph set"

Maybe this is your problem?

Otherwise send me a concrete lemma which leads to a concrete error message, so 
that I can give you a more concrete answer...


   Norbert





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