# Theory Lemmas

Up to index of Isabelle/HOLCF/IOA/NTP

theory Lemmas
imports Main
uses [Lemmas.ML]
begin

    (*  Title:      HOL/IOA/NTP/Lemmas.thy
        ID:         $Id: Lemmas.thy,v 1.6 2005/09/03 14:50:24 wenzelm Exp $
        Author:     Tobias Nipkow & Konrad Slind
    *)

    theory Lemmas
    imports Main
    begin

    end

theorem neg_flip:

      (X = (¬ Y)) = ((¬ X) = Y)

theorem pred_suc:

      0 < x ==> (x - 1 = y) = (x = Suc y)