# Tag Info

Accepted

### Why is Isabelle usually not just Isabelle but Isabelle/<xyz>?

Isabelle the program is designed as a "generic" LCF-style proof assistant/logical framework; it gives you a very minimal base logic (based on Church's simple type theory (pdf) and called ...
• 297

### Why is Isabelle usually not just Isabelle but Isabelle/<xyz>?

There are many more, notably: Isabelle/Pure (the core logic), Isabelle/jEdit (the bundled IDE), Isabelle/ML (its version of the ML language and its libraries), Isabelle/Scala (same for Scala), I ...
• 1,013
Accepted

### Is there a way to use sledgehammer in Isar proofs?

It will work in an Isar proof, however you will want to pull a subgoal into focus. Unless your most recent tactic is something like induction, you will find ...
• 1,128

### Is there an elegant way of proving an equality A=B by going in both directions?

I believe there is, provided that L and R are predicates, of course: ...

### Result contains obtained parameters? So what?

This one was already answered on Stack Overflow: Soundness of natural deduction requires that you get hold of the witness before you open the existential quantifier. This means you need to place the ...
• 495
Accepted

### How to write a low-level proof in Isar?

One way to accomplish this, somewhat in the lines of what you did, is the following: ...
• 1,013
1 vote

### What is an assumption in Isar?

I assume the question is about how assumptions can be referenced to in an Isar proof. One way to use assumptions is through the assms keyword like this: ...
• 126
1 vote

### Type class constaint is ignored in type synonym definition

Yes, datatype is adequate for this: datatype ('v::group_add) myTypeOperator = MyTyOp 'v datatype ('v) myTypeOperator2 = MyTyOp2 "'v::group_add" Type ...
• 311
1 vote
Accepted

### Picking this and calculation in Isabelle/JEdit output

At each step accumulating facts (i.e., each of moreover and the final ultimately), the proof state will show the fact ...
• 1,013

Only top scored, non community-wiki answers of a minimum length are eligible