Isabelle as a solver in Leon
Showing
- .gitignore 3 additions, 0 deletions.gitignore
- .gitmodules 3 additions, 0 deletions.gitmodules
- ROOTS 2 additions, 0 deletionsROOTS
- build.sbt 12 additions, 9 deletionsbuild.sbt
- library/annotation/isabelle.scala 31 additions, 0 deletionslibrary/annotation/isabelle.scala
- library/collection/List.scala 25 additions, 2 deletionslibrary/collection/List.scala
- library/lang/Dummy.scala 3 additions, 0 deletionslibrary/lang/Dummy.scala
- library/lang/Map.scala 5 additions, 4 deletionslibrary/lang/Map.scala
- library/lang/Option.scala 6 additions, 0 deletionslibrary/lang/Option.scala
- library/monads/state/State.scala 6 additions, 5 deletionslibrary/monads/state/State.scala
- src/main/isabelle/.gitignore 1 addition, 0 deletionssrc/main/isabelle/.gitignore
- src/main/isabelle/Leon.thy 5 additions, 0 deletionssrc/main/isabelle/Leon.thy
- src/main/isabelle/Leon_Library.thy 29 additions, 0 deletionssrc/main/isabelle/Leon_Library.thy
- src/main/isabelle/Leon_Ops.thy 47 additions, 0 deletionssrc/main/isabelle/Leon_Ops.thy
- src/main/isabelle/ROOT 8 additions, 0 deletionssrc/main/isabelle/ROOT
- src/main/isabelle/leon_syntax.ML 82 additions, 0 deletionssrc/main/isabelle/leon_syntax.ML
- src/main/isabelle/stateful_ops.ML 565 additions, 0 deletionssrc/main/isabelle/stateful_ops.ML
- src/main/isabelle/stateless_ops.ML 40 additions, 0 deletionssrc/main/isabelle/stateless_ops.ML
- src/main/isabelle/tactics.ML 67 additions, 0 deletionssrc/main/isabelle/tactics.ML
- src/main/isabelle/term_codec.ML 75 additions, 0 deletionssrc/main/isabelle/term_codec.ML
Loading
Please register or sign in to comment