32 |
32 |
33 val proofT = Type ("proof", []); |
33 val proofT = Type ("proof", []); |
34 val paramT = Type ("param", []); |
34 val paramT = Type ("param", []); |
35 val paramsT = Type ("params", []); |
35 val paramsT = Type ("params", []); |
36 val idtT = Type ("idt", []); |
36 val idtT = Type ("idt", []); |
37 val aT = TFree ("'a", ["logic"]); |
37 val aT = TFree ("'a", []); |
38 |
38 |
39 (** constants for theorems and axioms **) |
39 (** constants for theorems and axioms **) |
40 |
40 |
41 fun add_prefix a b = NameSpace.pack (a :: NameSpace.unpack b); |
41 fun add_prefix a b = NameSpace.pack (a :: NameSpace.unpack b); |
42 |
42 |
47 |
47 |
48 fun add_proof_syntax sg = |
48 fun add_proof_syntax sg = |
49 sg |
49 sg |
50 |> Sign.copy |
50 |> Sign.copy |
51 |> Sign.add_path "/" |
51 |> Sign.add_path "/" |
52 |> Sign.add_defsort_i ["logic"] |
52 |> Sign.add_defsort_i [] |
53 |> Sign.add_types [("proof", 0, NoSyn)] |
53 |> Sign.add_types [("proof", 0, NoSyn)] |
54 |> Sign.add_arities [("proof", [], "logic")] |
|
55 |> Sign.add_consts_i |
54 |> Sign.add_consts_i |
56 [("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)), |
55 [("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)), |
57 ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4)), |
56 ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4)), |
58 ("Abst", (aT --> proofT) --> proofT, NoSyn), |
57 ("Abst", (aT --> proofT) --> proofT, NoSyn), |
59 ("AbsP", [propT, proofT --> proofT] ---> proofT, NoSyn), |
58 ("AbsP", [propT, proofT --> proofT] ---> proofT, NoSyn), |