Re: [isabelle] Accessing split-theorems on ML-level
Yes, this is not quite what I had in mind though. In my program, I have
a type (from some variable in a term) and I would like to get the split
theorem directly from the type, without having to create a string
representation of the name of that type.
Amine Chaieb wrote:
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