removed deriv.ML which is now incorporated into thm.ML;
authorwenzelm
Mon Sep 22 15:26:11 2008 +0200 (2008-09-22)
changeset 283186b8d001ce1de
parent 28317 83c4fc383409
child 28319 13cb2108c2b9
removed deriv.ML which is now incorporated into thm.ML;
src/Pure/IsaMakefile
src/Pure/ROOT.ML
src/Pure/deriv.ML
     1.1 --- a/src/Pure/IsaMakefile	Mon Sep 22 15:26:11 2008 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Mon Sep 22 15:26:11 2008 +0200
     1.3 @@ -76,14 +76,13 @@
     1.4    Thy/thy_output.ML Tools/ROOT.ML Tools/invoke.ML Tools/quickcheck.ML	\
     1.5    Tools/value.ML Tools/isabelle_process.ML Tools/named_thms.ML		\
     1.6    Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML config.ML	\
     1.7 -  conjunction.ML consts.ML context.ML conv.ML defs.ML deriv.ML		\
     1.8 -  display.ML drule.ML envir.ML facts.ML goal.ML interpretation.ML	\
     1.9 -  library.ML logic.ML meta_simplifier.ML more_thm.ML morphism.ML	\
    1.10 -  name.ML net.ML old_goals.ML pattern.ML primitive_defs.ML		\
    1.11 -  proofterm.ML pure_setup.ML pure_thy.ML search.ML sign.ML		\
    1.12 -  simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML term.ML	\
    1.13 -  term_subst.ML theory.ML thm.ML type.ML type_infer.ML unify.ML		\
    1.14 -  variable.ML
    1.15 +  conjunction.ML consts.ML context.ML conv.ML defs.ML display.ML	\
    1.16 +  drule.ML envir.ML facts.ML goal.ML interpretation.ML library.ML	\
    1.17 +  logic.ML meta_simplifier.ML more_thm.ML morphism.ML name.ML net.ML	\
    1.18 +  old_goals.ML pattern.ML primitive_defs.ML proofterm.ML pure_setup.ML	\
    1.19 +  pure_thy.ML search.ML sign.ML simplifier.ML sorts.ML subgoal.ML	\
    1.20 +  tactic.ML tctical.ML term.ML term_subst.ML theory.ML thm.ML type.ML	\
    1.21 +  type_infer.ML unify.ML variable.ML
    1.22  	@./mk
    1.23  
    1.24  
     2.1 --- a/src/Pure/ROOT.ML	Mon Sep 22 15:26:11 2008 +0200
     2.2 +++ b/src/Pure/ROOT.ML	Mon Sep 22 15:26:11 2008 +0200
     2.3 @@ -61,7 +61,6 @@
     2.4  use "theory.ML";
     2.5  use "interpretation.ML";
     2.6  use "proofterm.ML";
     2.7 -use "deriv.ML";
     2.8  use "thm.ML";
     2.9  use "more_thm.ML";
    2.10  use "facts.ML";
     3.1 --- a/src/Pure/deriv.ML	Mon Sep 22 15:26:11 2008 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,36 +0,0 @@
     3.4 -(*  Title:      Pure/deriv.ML
     3.5 -    ID:         $Id$
     3.6 -    Author:     Makarius
     3.7 -
     3.8 -Abstract derivations based on raw proof terms.
     3.9 -*)
    3.10 -
    3.11 -signature DERIV =
    3.12 -sig
    3.13 -  type T
    3.14 -  val oracle_of: T -> bool
    3.15 -  val proof_of: T -> Proofterm.proof
    3.16 -  val uncond_rule: (Proofterm.proof -> Proofterm.proof) -> T -> T
    3.17 -  val rule0: Proofterm.proof -> T
    3.18 -  val rule1: (Proofterm.proof -> Proofterm.proof) -> T -> T
    3.19 -  val rule2: (Proofterm.proof -> Proofterm.proof -> Proofterm.proof) -> T -> T -> T
    3.20 -  val oracle: string -> term -> T
    3.21 -end;
    3.22 -
    3.23 -structure Deriv: DERIV =
    3.24 -struct
    3.25 -
    3.26 -datatype T = Der of bool * Proofterm.proof;
    3.27 -
    3.28 -fun oracle_of (Der (ora, _)) = ora;
    3.29 -fun proof_of (Der (_, proof)) = proof;
    3.30 -
    3.31 -fun uncond_rule f (Der (ora, prf)) = Der (ora, f prf);
    3.32 -
    3.33 -fun rule0 prf = Der (Proofterm.infer_derivs' I (false, prf));
    3.34 -fun rule1 f (Der der) = Der (Proofterm.infer_derivs' f der);
    3.35 -fun rule2 f (Der der1) (Der der2) = Der (Proofterm.infer_derivs f der1 der2);
    3.36 -
    3.37 -fun oracle name prop = Der (true, Proofterm.oracle_proof name prop);
    3.38 -
    3.39 -end;