Re: [isabelle] Accessing split-theorems on ML-level
In ML you can access facts in the theorem databaase using thm or thms,
when the result is a theorem list.
In you case , e.g.
ML> thm "list.split";
val it =
"?P (list_case ?f1.0 ?f2.0 ?x) =
((?x =  --> ?P ?f1.0) &
(ALL a list. ?x = a # list --> ?P (?f2.0 a list)))" : Thm.thm
Moa Johansson wrote:
I need to get hold of theorems for splitting case-statements, given a
datatype, on the ML level (eg. theorems like "list.split", "nat.split"
etc). Where can I find these?
This archive was generated by a fusion of
Pipermail (Mailman edition) and