src/Pure/object_logic.ML
author wenzelm
Mon Nov 09 15:42:08 1998 +0100 (1998-11-09)
changeset 5840 e2d2b896c717
child 6768 26d64339c25a
permissions -rw-r--r--
Object logic specific operations.
     1 (*  Title:      Pure/object_logic.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Object logic specific operations.
     6 
     7 TODO:
     8   - theory data instead of hardwired operations (!!);
     9 *)
    10 
    11 signature OBJECT_LOGIC =
    12 sig
    13   val dest_statement: string * term -> (string * term) list
    14   val setup: (theory -> theory) list
    15 end;
    16 
    17 structure ObjectLogic: OBJECT_LOGIC =
    18 struct
    19 
    20 
    21 fun dest_statement (name, prop) =
    22   let val concl = Logic.strip_imp_concl prop in
    23     [(name ^ "_prop", prop), (name ^ "_concl", concl)] @
    24       (case concl of Const ("Trueprop", _) $ t => [(name, t)] | _ => [])
    25   end;
    26 
    27 
    28 (* FIXME *)
    29 val setup = [];
    30 
    31 end;