src/Pure/deriv.ML
changeset 28318 6b8d001ce1de
parent 28317 83c4fc383409
child 28319 13cb2108c2b9
     1.1 --- a/src/Pure/deriv.ML	Mon Sep 22 15:26:11 2008 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,36 +0,0 @@
     1.4 -(*  Title:      Pure/deriv.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Makarius
     1.7 -
     1.8 -Abstract derivations based on raw proof terms.
     1.9 -*)
    1.10 -
    1.11 -signature DERIV =
    1.12 -sig
    1.13 -  type T
    1.14 -  val oracle_of: T -> bool
    1.15 -  val proof_of: T -> Proofterm.proof
    1.16 -  val uncond_rule: (Proofterm.proof -> Proofterm.proof) -> T -> T
    1.17 -  val rule0: Proofterm.proof -> T
    1.18 -  val rule1: (Proofterm.proof -> Proofterm.proof) -> T -> T
    1.19 -  val rule2: (Proofterm.proof -> Proofterm.proof -> Proofterm.proof) -> T -> T -> T
    1.20 -  val oracle: string -> term -> T
    1.21 -end;
    1.22 -
    1.23 -structure Deriv: DERIV =
    1.24 -struct
    1.25 -
    1.26 -datatype T = Der of bool * Proofterm.proof;
    1.27 -
    1.28 -fun oracle_of (Der (ora, _)) = ora;
    1.29 -fun proof_of (Der (_, proof)) = proof;
    1.30 -
    1.31 -fun uncond_rule f (Der (ora, prf)) = Der (ora, f prf);
    1.32 -
    1.33 -fun rule0 prf = Der (Proofterm.infer_derivs' I (false, prf));
    1.34 -fun rule1 f (Der der) = Der (Proofterm.infer_derivs' f der);
    1.35 -fun rule2 f (Der der1) (Der der2) = Der (Proofterm.infer_derivs f der1 der2);
    1.36 -
    1.37 -fun oracle name prop = Der (true, Proofterm.oracle_proof name prop);
    1.38 -
    1.39 -end;