src/Pure/ProofGeneral/pgip_input.ML
changeset 23436 343e84195e2c
parent 22406 a591df440b5b
child 26548 41bbcaf3e481
     1.1 --- a/src/Pure/ProofGeneral/pgip_input.ML	Wed Jun 20 15:10:02 2007 +0200
     1.2 +++ b/src/Pure/ProofGeneral/pgip_input.ML	Wed Jun 20 15:10:34 2007 +0200
     1.3 @@ -19,10 +19,6 @@
     1.4      (* prover control *)
     1.5      | Proverinit     of { }
     1.6      | Proverexit     of { }
     1.7 -    | Startquiet     of { }
     1.8 -    | Stopquiet      of { } 
     1.9 -    | Pgmlsymbolson  of { } 
    1.10 -    | Pgmlsymbolsoff of { }
    1.11      | Setproverflag  of { flagname:string, value: bool }
    1.12      (* improper proof commands: control proof state *)
    1.13      | Dostep         of { text: string }
    1.14 @@ -88,10 +84,6 @@
    1.15         (* prover control *)
    1.16         | Proverinit 	of { }
    1.17         | Proverexit 	of { }
    1.18 -       | Startquiet 	of { }
    1.19 -       | Stopquiet	of { } 
    1.20 -       | Pgmlsymbolson  of { } 
    1.21 -       | Pgmlsymbolsoff of { }
    1.22         | Setproverflag  of { flagname:string, value: bool }
    1.23         (* improper proof commands: control proof state *)
    1.24         | Dostep		of { text: string }
    1.25 @@ -186,10 +178,6 @@
    1.26     (* provercontrol *)
    1.27     | "proverinit"     => Proverinit { }
    1.28     | "proverexit"     => Proverexit { }
    1.29 -   | "startquiet"     => Startquiet { }
    1.30 -   | "stopquiet"      => Stopquiet { }
    1.31 -   | "pgmlsymbolson"  => Pgmlsymbolson { }
    1.32 -   | "pgmlsymbolsoff" => Pgmlsymbolsoff { }
    1.33     | "setproverflag"  => Setproverflag { flagname = flagname_attr attrs,
    1.34  					 value = read_pgipbool (value_attr attrs) }
    1.35     (* improperproofcmd: improper commands not in script *)