Hi, I'm trying to generate a proof goal from string using the following:
fun generate x lthy = let val thy = Local_Theory.exit_global lthy val ctxt = ProofContext.init_global thy in (Specification.theorem_cmd Thm.lemmaK NONE (K I) (Binding.name "", []) [] (Element.Shows [(Attrib.empty_binding, [(Syntax.string_of_term ctxt @{term "F"} ^ " = " ^ Syntax.string_of_term ctxt @{term "G"} , [])])]) x lthy) end val _ = Outer_Syntax.local_theory_to_proof' "generate" Thm.lemmaK Keyword.thy_goal (Scan.succeed generate) Unfortunately I keep getting an error saying: *** Malformed YXML encoding: multiple results *** At command "verify_with" But, if I change the generate function to fun generate x lthy = let val thy = Local_Theory.exit_global lthy val ctxt = ProofContext.init_global thy in (Specification.theorem_cmd Thm.lemmaK NONE (K I) (Binding.name "", []) [] (Element.Shows [(Attrib.empty_binding, [((Syntax.string_of_term ctxt @{term "F = G"}) , [])])]) x lthy) end then the proof goal is properly generated. Notice that in the second version, the string is created from a single term on the string "F = G", whereas the string in the first is created by concatenating together 3 individual strings: string of @{term "F"}, "=", and string of @{term "G"}. How come there is a difference? This is just a toy example, because I'm actually dealing with variable terms, so it's not as simple as "F" and "G". Please help. Thanks. Steve
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev