Logo Questions Linux Laravel Mysql Ubuntu Git Menu
HTML CSS JAVASCRIPT SQL PYTHON PHP BOOTSTRAP JAVA JQUERY R React Kotlin
 

New posts in isabelle

A theorem prover / proof assistant supporting (multiple) subtyping / subclassing [closed]

haskell coq isabelle agda theorem-proving

Isabelle solvers: "auto" or "fastforce"? (comparison of solver strength)

solver isabelle theorem-proving

Is there a way to split conjunction automatically?

isabelle

Isabelle: Unsupported recursive occurrence of a datatype via type constructor "Set.set"

recursion isabelle theorem-proving

The order of premises

isabelle

How do you print local variables and ?thesis in an Isabelle proof (debugging in Isabelle)?

isabelle theorem-proving

How can I use rules suggested by solve_direct? (by (rule …) doesn't always work)

solver proof isabelle theorem-proving

Isabelle/HOL: What does the THE construct denote?

isabelle

How do I display brackets around assumptions in Isabelle/jEdit?

jedit isabelle proof-general

Is there a way to get a complete list of all kinds of operators/constructors of Isabelle?

isabelle

verify an Isabelle proof from the command line

command-line isabelle

Bad theory import in isabelle

isabelle

Max of set in Isabelle

choice isabelle

Building a session using `isabelle` vs jEdit

isabelle jedit

Automatic translation from Isabelle/HOL to HOL

isabelle hol

Partial function in Coq / underdefined?

compiler-construction isabelle agda

Apply a method if and only if it solves the current goal

proof isabelle

Defining overloaded constants in Isabelle

overloading isabelle

What is the difference between primrec and fun in Isabelle/HOL?

isabelle
« Newer Entries Older Entries »