Language for the Hets command line interface

SCRIPT ::= COMMAND*
COMMAND ::= 
       -- commands for development graph mode
            use PATH            -- open a file with a HetCASL library
                                -- this will compute a development graph
                                -- and a list of open proof obligations
                                -- also all referenced libraries need to be loaded
                                -- (and this needs to be communicated to PGIP)
          | dg DG-COMMAND GOAL* -- apply a proof step of the dg calculus
                                -- if no goal is specified, the first goals is tried
          | dg-all DG-COMMAN    -- same, but for all open goals
          | show-dg-goals       -- display list of open dg goals
       -- commands for theory mode
          | show-theory-goals   -- display list of theory goals
          | show-theory         -- show current theory and proof goals
          | node-info           -- show info about current dg node (name, origin, sublogic)
          | show-taxonomy       -- show taxonomy graph
          | show-concepts       -- show conecpt graph
          | translate COMORPHISM -- translate theory goals along comorphism
          | prover PROVER        -- select a prover
          | proof-script FORMULA PROOF-SCRIPT end-script
                                 -- process proof script for one goal
          | cons-check PROVER    -- check consistency
       -- interactive commands for theory mode
          | prove FORMULA* AXIOM-SELECTION?
                -- insert initial proof script
                -- insert only the specified formulas as goals (top goal if none is specified) 
                -- insert only the specified axioms (otherwise, insert all axioms)
          | prove-all AXIOM-SELECTION?
                -- same for all goals

AXIOM-SELECTION ::=
            with FORMULA+                        -- include only specified axioms
          | exlcuding FORMULA+                   -- exlcude specified axioms

PROOF-SCRIPT                  -- can be anything (prover specific)
                              -- the end is recognized with "end-script"

DG-COMMAND ::= auto         -- automatic tactic
             | glob-subsume -- global subsumption
             | glob-decomp  -- global decomposition
             | loc-infer    -- local inference
             | loc-decomp   -- local decomposition
             | comp         -- composition
             | comp-new     -- composition with speculation of new egdes
             | hide-thm     -- Hide-Theorem-Shift
             | thm-hide     -- Theorem-Hide-Shift
             | basic        -- start proving at a particular node,
                            -- i.e. start local proving in a theory

GOAL ::= NODE             -- select local goals at a node
       | NODE -> NODE     -- select all edges between two given nodes
       | NODE - DIGIT* -> NODE  -- select specific edge between two nodes
NODE       ::= ID         -- specify nodes with their names 
COMORPHISM ::= ID ; ... ; ID    -- composite of basic comorphisms
                                -- if jsut one logic name is given, the default is used
PROVER ::= ID                   -- name of prover
FORMULA ::= ID                  -- label of formula
PATH ::=                        -- path name (look at CASL syntax)
ID ::=                          -- identifier (look at CASL syntax)