Added constants for Hyp, Oracle and MinProof.
authorberghofe
Fri May 31 18:52:23 2002 +0200 (2002-05-31)
changeset 1319918402c1f76bf
parent 13198 3e40f48a500f
child 13200 7618f289c9c1
Added constants for Hyp, Oracle and MinProof.
src/Pure/Proof/proof_syntax.ML
     1.1 --- a/src/Pure/Proof/proof_syntax.ML	Fri May 31 18:50:03 2002 +0200
     1.2 +++ b/src/Pure/Proof/proof_syntax.ML	Fri May 31 18:52:23 2002 +0200
     1.3 @@ -56,7 +56,10 @@
     1.4        [("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)),
     1.5         ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4)),
     1.6         ("Abst", (aT --> proofT) --> proofT, NoSyn),
     1.7 -       ("AbsP", [propT, proofT --> proofT] ---> proofT, NoSyn)]
     1.8 +       ("AbsP", [propT, proofT --> proofT] ---> proofT, NoSyn),
     1.9 +       ("Hyp", propT --> proofT, NoSyn),
    1.10 +       ("Oracle", propT --> proofT, NoSyn),
    1.11 +       ("MinProof", proofT, Delimfix "?")]
    1.12    |> Sign.add_nonterminals ["param", "params"]
    1.13    |> Sign.add_syntax_i
    1.14        [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)),
    1.15 @@ -150,6 +153,7 @@
    1.16                         | None => error ("Unknown theorem " ^ quote name)))
    1.17                   end
    1.18               | _ => error ("Illegal proof constant name: " ^ quote s))
    1.19 +      | prf_of Ts (Const ("Hyp", _) $ prop) = Hyp prop
    1.20        | prf_of Ts (v as Var ((_, Type ("proof", _)))) = Hyp v
    1.21        | prf_of [] (Const ("Abst", _) $ Abs (s, T, prf)) =
    1.22            Abst (s, if ty then Some T else None,
    1.23 @@ -174,9 +178,9 @@
    1.24  
    1.25  val AbsPt = Const ("AbsP", [propT, proofT --> proofT] ---> proofT);
    1.26  val AppPt = Const ("AppP", [proofT, proofT] ---> proofT);
    1.27 -val Hypt = Free ("Hyp", propT --> proofT);
    1.28 -val Oraclet = Free ("Oracle", propT --> proofT);
    1.29 -val MinProoft = Free ("?", proofT);
    1.30 +val Hypt = Const ("Hyp", propT --> proofT);
    1.31 +val Oraclet = Const ("Oracle", propT --> proofT);
    1.32 +val MinProoft = Const ("MinProof", proofT);
    1.33  
    1.34  val mk_tyapp = foldl (fn (prf, T) => Const ("Appt",
    1.35    [proofT, itselfT T] ---> proofT) $ prf $ Logic.mk_type T);