src/Pure/Isar/object_logic.ML
author wenzelm
Mon, 22 Oct 2001 18:07:53 +0200
changeset 11897 b9f2028f53bd
child 12123 739eba13e2cd
permissions -rw-r--r--
moved object_logic.ML to Isar/object_logic.ML;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11897
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/object_logic.ML
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
     5
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
     6
Specifics about common object-logics.
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
     7
*)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
     8
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
     9
signature OBJECT_LOGIC =
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    10
sig
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    11
  val add_judgment: bstring * string * mixfix -> theory -> theory
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    12
  val add_judgment_i: bstring * typ * mixfix -> theory -> theory
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    13
  val judgment_name: Sign.sg -> string
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    14
  val is_judgment: Sign.sg -> term -> bool
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    15
  val drop_judgment: Sign.sg -> term -> term
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    16
  val fixed_judgment: Sign.sg -> string -> term
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    17
  val declare_atomize: theory attribute
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    18
  val declare_rulify: theory attribute
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    19
  val atomize_tac: int -> tactic
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    20
  val atomize_goal: int -> thm -> thm
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    21
  val rulify: thm -> thm
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    22
  val rulify_no_asm: thm -> thm
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    23
  val rule_format: 'a attribute
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    24
  val rule_format_no_asm: 'a attribute
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    25
  val setup: (theory -> theory) list
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    26
end;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    27
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    28
structure ObjectLogic: OBJECT_LOGIC =
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    29
struct
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    30
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    31
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    32
(** object-logic theory data **)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    33
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    34
(* data kind 'Pure/object-logic' *)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    35
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    36
structure ObjectLogicDataArgs =
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    37
struct
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    38
  val name = "Pure/object-logic";
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    39
  type T = string option * (thm list * thm list);
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    40
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    41
  val empty = (None, ([], [Drule.norm_hhf_eq]));
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    42
  val copy = I;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    43
  val prep_ext = I;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    44
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    45
  fun merge_judgment (Some x, Some y) =
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    46
        if x = y then Some x else error "Attempt to merge different object-logics"
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    47
    | merge_judgment (j1, j2) = if is_some j1 then j1 else j2;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    48
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    49
  fun merge ((judgment1, (atomize1, rulify1)), (judgment2, (atomize2, rulify2))) =
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    50
    (merge_judgment (judgment1, judgment2),
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    51
      (Drule.merge_rules (atomize1, atomize2), Drule.merge_rules (rulify1, rulify2)));
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    52
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    53
  fun print _ _ = ();
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    54
end;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    55
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    56
structure ObjectLogicData = TheoryDataFun(ObjectLogicDataArgs);
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    57
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    58
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    59
(** generic treatment of judgments -- with a single argument only **)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    60
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    61
(* add_judgment(_i) *)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    62
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    63
local
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    64
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    65
fun new_judgment name (None, rules) = (Some name, rules)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    66
  | new_judgment _ (Some _, _) = error "Attempt to redeclare object-logic judgment";
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    67
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    68
fun gen_add_judgment add_consts (name, T, syn) thy =
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    69
  thy
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    70
  |> add_consts [(name, T, syn)]
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    71
  |> ObjectLogicData.map (new_judgment (Sign.full_name (Theory.sign_of thy) name));
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    72
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    73
in
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    74
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    75
val add_judgment = gen_add_judgment Theory.add_consts;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    76
val add_judgment_i = gen_add_judgment Theory.add_consts_i;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    77
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    78
end;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    79
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    80
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    81
(* term operations *)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    82
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    83
fun judgment_name sg =
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    84
  (case ObjectLogicData.get_sg sg of
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    85
    (Some name, _) => name
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    86
  | _ => raise TERM ("Unknown object-logic judgment", []));
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    87
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    88
fun is_judgment sg (Const (c, _) $ _) = c = judgment_name sg
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    89
  | is_judgment _ _ = false;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    90
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    91
fun drop_judgment sg (Abs (x, T, t)) = Abs (x, T, drop_judgment sg t)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    92
  | drop_judgment sg (tm as (Const (c, _) $ t)) = if c = judgment_name sg then t else tm
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    93
  | drop_judgment _ tm = tm;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    94
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    95
fun fixed_judgment sg x =
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    96
  let  (*be robust wrt. low-level errors*)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    97
    val c = judgment_name sg;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    98
    val aT = TFree ("'a", logicS);
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
    99
    val T =
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   100
      if_none (Sign.const_type sg c) (aT --> propT)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   101
      |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   102
    val U = Term.domain_type T handle Match => aT;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   103
  in Const (c, T) $ Free (x, U) end;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   104
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   105
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   106
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   107
(** treatment of meta-level connectives **)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   108
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   109
(* maintain rules *)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   110
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   111
val get_atomize = #1 o #2 o ObjectLogicData.get_sg;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   112
val get_rulify = #2 o #2 o ObjectLogicData.get_sg;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   113
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   114
val add_atomize = ObjectLogicData.map o Library.apsnd o Library.apfst o Drule.add_rules;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   115
val add_rulify = ObjectLogicData.map o Library.apsnd o Library.apsnd o Drule.add_rules;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   116
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   117
fun declare_atomize (thy, th) = (add_atomize [th] thy, th);
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   118
fun declare_rulify (thy, th) = (add_rulify [th] thy, th);
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   119
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   120
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   121
(* atomize *)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   122
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   123
fun rewrite_prems_tac rews i = PRIMITIVE (MetaSimplifier.fconv_rule
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   124
  (MetaSimplifier.goals_conv (Library.equal i)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   125
    (MetaSimplifier.forall_conv
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   126
      (MetaSimplifier.goals_conv (K true) (Tactic.rewrite true rews)))));
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   127
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   128
fun atomize_tac i st =
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   129
  if Logic.has_meta_prems (#prop (Thm.rep_thm st)) i then
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   130
    (rewrite_prems_tac (get_atomize (Thm.sign_of_thm st)) i) st
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   131
  else all_tac st;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   132
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   133
fun atomize_goal i st =
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   134
  (case Seq.pull (atomize_tac i st) of None => st | Some (st', _) => st');
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   135
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   136
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   137
(* rulify *)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   138
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   139
fun gen_rulify full thm =
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   140
  Tactic.simplify full (get_rulify (Thm.sign_of_thm thm)) thm
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   141
  |> Drule.forall_elim_vars_safe |> Drule.strip_shyps_warning |> Drule.zero_var_indexes;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   142
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   143
val rulify = gen_rulify true;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   144
val rulify_no_asm = gen_rulify false;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   145
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   146
fun rule_format x = Drule.rule_attribute (fn _ => rulify) x;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   147
fun rule_format_no_asm x = Drule.rule_attribute (fn _ => rulify_no_asm) x;
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   148
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   149
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   150
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   151
(** theory setup **)
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   152
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   153
val setup = [ObjectLogicData.init];
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   154
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   155
b9f2028f53bd moved object_logic.ML to Isar/object_logic.ML;
wenzelm
parents:
diff changeset
   156
end;