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