All Questions
Tagged with isar isabelle-hol
4 questions
1
vote
1
answer
154
views
Result contains obtained parameters? So what?
When proving an existential claim, you can use rule exI and exhibit an example; this is a sufficient proof (as you'd expect!). Conversely, if you have an ...
- 515
1
vote
1
answer
36
views
Type class constaint is ignored in type synonym definition
My class constraint is ignored in a type synonym definition: for
type_synonym 'value myTypeOperator = "'value::group_add"
I get
...
- 323
1
vote
1
answer
81
views
8
votes
1
answer
205
views
Is there an elegant way of proving an equality A=B by going in both directions?
I would like to prove an equality by splitting it into a proof in each direction.
Is there a more elegant style to start such a proof than this way::
...
- 81