Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 148
    • Issues 148
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 8
    • Merge requests 8
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Repository

Switch branch/tag
  • iris
  • theories
  • tests
  • proofmode.v
Find file BlameHistoryPermalink
  • Ralf Jung's avatar
    Revert "Use implication in core so that we can test it.", add a dedicated test · 16c90c69
    Ralf Jung authored Mar 08, 2018
    This reverts commit daaabf41.  We have tests for
    testcase, we shouldn't depend on using arcane features in our definitions for
    this purpose.  Also, this exposes that there still is a bug somewhere (see the
    FIXME).
    16c90c69

Replace proofmode.v

Attach a file by drag & drop or click to upload


Cancel
GitLab will create a branch in your fork and start a merge request.