0N/A{- |

0N/AModule : $Header$

0N/ACopyright : (c) Andy Gimblett, Liam O'Reilly and Markus Roggenbach, Swansea University 2008

0N/ALicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

0N/A

2362N/AMaintainer : csliam@swansea.ac.uk

0N/AStability : provisional

2362N/APortability : portable

0N/A

0N/AData structures for Isabelle Proofs

0N/A-}

0N/A

0N/Amodule Isabelle.IsaProof where

0N/A

0N/Adata IsaProof = IsaProof

0N/A { proof :: [ProofCommand],

0N/A end :: ProofEnd

0N/A } deriving (Show, Eq, Ord)

0N/A

2362N/Adata ProofCommand

2362N/A = Apply ProofMethod

2362N/A | Back

0N/A | Defer Int

0N/A -- | Pr Int -- This proof command simply sets the number of

0N/A -- goals shown in the display and is not needed

0N/A | Prefer Int

0N/A | Refute

0N/A deriving (Show, Eq, Ord)

0N/A

0N/Adata ProofEnd

0N/A = By ProofMethod

0N/A | Done

0N/A | Oops

0N/A | Sorry

1693N/A deriving (Show, Eq, Ord)

1693N/A

1693N/Adata ProofMethod

1693N/A = Auto -- This is a plain auto with no parameters - it is used

1693N/A -- so often it warents its own constructor

0N/A | Simp -- This is a plain auto with no parameters - it is used

0N/A -- so often it warents its own constructor

0N/A | Other String -- used for proof methods that have not been

0N/A -- implemented yet - including auto and simp

0N/A -- with parameters

0N/A deriving (Show, Eq, Ord)

1693N/A