Re: [isabelle] What is sumC?



I'm not sure I fully understand the requirement. Are you looking for a
proof method which can solve the full goal automatically? If so, you can
try 'code_simp' or 'eval'.

Where is code_simp described? It's not in "Programming and Proving in Isabelle/HOL"; it's not in "The Isabelle/Isar Reference Manual"; it's not in "The Isabelle/Isar Implementation"; it's not in "Isabelle/HOL -- A Proof Assistant for Higher-Order Logic." Are there other manuals or tutorials I should try?
--
Prof. W. Douglas Maurer                Washington, DC 20052, USA
Department of Computer Science         Tel. (1-202)994-5921
The George Washington University       Fax  (1-202)994-4875




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