src/Pure/object_logic.ML
changeset 5840 e2d2b896c717
child 6768 26d64339c25a
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/object_logic.ML	Mon Nov 09 15:42:08 1998 +0100
     1.3 @@ -0,0 +1,31 @@
     1.4 +(*  Title:      Pure/object_logic.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Markus Wenzel, TU Muenchen
     1.7 +
     1.8 +Object logic specific operations.
     1.9 +
    1.10 +TODO:
    1.11 +  - theory data instead of hardwired operations (!!);
    1.12 +*)
    1.13 +
    1.14 +signature OBJECT_LOGIC =
    1.15 +sig
    1.16 +  val dest_statement: string * term -> (string * term) list
    1.17 +  val setup: (theory -> theory) list
    1.18 +end;
    1.19 +
    1.20 +structure ObjectLogic: OBJECT_LOGIC =
    1.21 +struct
    1.22 +
    1.23 +
    1.24 +fun dest_statement (name, prop) =
    1.25 +  let val concl = Logic.strip_imp_concl prop in
    1.26 +    [(name ^ "_prop", prop), (name ^ "_concl", concl)] @
    1.27 +      (case concl of Const ("Trueprop", _) $ t => [(name, t)] | _ => [])
    1.28 +  end;
    1.29 +
    1.30 +
    1.31 +(* FIXME *)
    1.32 +val setup = [];
    1.33 +
    1.34 +end;