src/HOLCF/adm.ML
author nipkow
Sun, 22 Dec 2002 10:43:43 +0100
changeset 13763 f94b569cd610
parent 13480 bb72bd43c6c3
child 14643 130076a81b84
permissions -rw-r--r--
added print translations tha avoid eta contraction for important binders.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4039
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
     1
(*  Title:      HOLCF/adm.ML
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
     2
    ID:         $Id$
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
     3
    Author:     Stefan Berghofer, TU Muenchen
11540
23794728cdb7 fixed header;
wenzelm
parents: 8411
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
4039
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
     5
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
     6
Admissibility tactic.
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
     7
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
     8
Checks whether adm_subst theorem is applicable to the current proof
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
     9
state:
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
    10
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
    11
  [| cont t; adm P |] ==> adm (%x. P (t x))
3655
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    12
4039
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
    13
"t" is instantiated with a term of chain-finite type, so that
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4039
diff changeset
    14
adm_chfin can be applied:
4039
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
    15
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
    16
  adm (P::'a::{chfin,pcpo} => bool)
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
    17
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
    18
*)
3655
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    19
4039
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
    20
signature ADM =
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
    21
sig
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
    22
  val adm_tac: (int -> tactic) -> int -> tactic
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
    23
end;
3655
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    24
4039
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
    25
structure Adm: ADM =
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
    26
struct
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
    27
3655
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    28
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    29
(*** find_subterms t 0 []
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    30
     returns lists of terms with the following properties:
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    31
       1. all terms in the list are disjoint subterms of t
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    32
       2. all terms contain the variable which is bound at level 0
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    33
       3. all occurences of the variable which is bound at level 0
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    34
          are "covered" by a term in the list
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    35
     a list of integers is associated with every term which describes
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    36
     the "path" leading to the subterm (required for instantiation of
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    37
     the adm_subst theorem (see functions mk_term, inst_adm_subst_thm))
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    38
***)
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    39
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    40
fun find_subterms (Bound i) lev path =
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    41
      if i = lev then [[(Bound 0, path)]]
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    42
      else []
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    43
  | find_subterms (t as (Abs (_, _, t2))) lev path =
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    44
      if filter (fn x => x<=lev)
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    45
           (add_loose_bnos (t, 0, [])) = [lev] then
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    46
        [(incr_bv (~lev, 0, t), path)]::
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    47
        (find_subterms t2 (lev+1) (0::path))
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    48
      else find_subterms t2 (lev+1) (0::path)
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    49
  | find_subterms (t as (t1 $ t2)) lev path =
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    50
      let val ts1 = find_subterms t1 lev (0::path);
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    51
          val ts2 = find_subterms t2 lev (1::path);
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    52
          fun combine [] y = []
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    53
            | combine (x::xs) ys =
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    54
                (map (fn z => x @ z) ys) @ (combine xs ys)
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    55
      in
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    56
        (if filter (fn x => x<=lev)
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    57
              (add_loose_bnos (t, 0, [])) = [lev] then
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    58
           [[(incr_bv (~lev, 0, t), path)]]
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    59
         else []) @
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    60
        (if ts1 = [] then ts2
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    61
         else if ts2 = [] then ts1
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    62
         else combine ts1 ts2)
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    63
      end
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    64
  | find_subterms _ _ _ = [];
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    65
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    66
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    67
(*** make term for instantiation of predicate "P" in adm_subst theorem ***)
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    68
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    69
fun make_term t path paths lev =
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    70
  if path mem paths then Bound lev
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    71
  else case t of
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    72
      (Abs (s, T, t1)) => Abs (s, T, make_term t1 (0::path) paths (lev+1))
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    73
    | (t1 $ t2) => (make_term t1 (0::path) paths lev) $
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    74
                   (make_term t2 (1::path) paths lev)
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    75
    | t1 => t1;
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    76
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    77
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    78
(*** check whether all terms in list are equal ***)
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    79
4039
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
    80
fun eq_terms [] = true
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
    81
  | eq_terms (ts as (t, _) :: _) = forall (fn (t2, _) => t2 aconv t) ts;
3655
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    82
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    83
4039
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
    84
(*figure out internal names*)
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
    85
val chfin_pcpoS = Sign.intern_sort (sign_of HOLCF.thy) ["chfin", "pcpo"];
4005
8858c472691a internalized some names
oheimb
parents: 3655
diff changeset
    86
val cont_name = Sign.intern_const (sign_of HOLCF.thy) "cont";
4039
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
    87
val adm_name = Sign.intern_const (sign_of HOLCF.thy) "adm";
4005
8858c472691a internalized some names
oheimb
parents: 3655
diff changeset
    88
8858c472691a internalized some names
oheimb
parents: 3655
diff changeset
    89
3655
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    90
(*** check whether type of terms in list is chain finite ***)
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    91
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    92
fun is_chfin sign T params ((t, _)::_) =
7652
2db14b7298c6 Sign.of_sort;
wenzelm
parents: 4721
diff changeset
    93
  let val parTs = map snd (rev params)
2db14b7298c6 Sign.of_sort;
wenzelm
parents: 4721
diff changeset
    94
  in Sign.of_sort sign (fastype_of1 (T::parTs, t), chfin_pcpoS) end;
3655
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    95
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    96
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    97
(*** try to prove that terms in list are continuous
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    98
     if successful, add continuity theorem to list l ***)
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
    99
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   100
fun prove_cont tac sign s T prems params (l, ts as ((t, _)::_)) =
4039
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
   101
  let val parTs = map snd (rev params);
3655
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   102
       val contT = (T --> (fastype_of1 (T::parTs, t))) --> HOLogic.boolT;
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   103
       fun mk_all [] t = t
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   104
         | mk_all ((a,T)::Ts) t = (all T) $ (Abs (a, T, mk_all Ts t));
4005
8858c472691a internalized some names
oheimb
parents: 3655
diff changeset
   105
       val t = HOLogic.mk_Trueprop((Const (cont_name, contT)) $ (Abs(s, T, t)));
3655
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   106
       val t' = mk_all params (Logic.list_implies (prems, t));
13480
bb72bd43c6c3 use Tactic.prove instead of prove_goalw_cterm in internal proofs!
wenzelm
parents: 11630
diff changeset
   107
       val thm = Tactic.prove sign [] [] t' (K (tac 1));
4039
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
   108
  in (ts, thm)::l end
11630
b95f527482fc avoid handle _;
wenzelm
parents: 11540
diff changeset
   109
  handle ERROR_MESSAGE _ => l;
3655
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   110
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   111
8411
d30df828a974 Type.typ_match now uses Vartab instead of association lists.
berghofe
parents: 7652
diff changeset
   112
(*** instantiation of adm_subst theorem (a bit tricky) ***)
3655
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   113
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   114
fun inst_adm_subst_thm state i params s T subt t paths =
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   115
  let val {sign, maxidx, ...} = rep_thm state;
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   116
      val j = maxidx+1;
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   117
      val {tsig, ...} = Sign.rep_sg sign;
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   118
      val parTs = map snd (rev params);
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   119
      val rule = lift_rule (state, i) adm_subst;
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   120
      val types = the o (fst (types_sorts rule));
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   121
      val tT = types ("t", j);
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   122
      val PT = types ("P", j);
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   123
      fun mk_abs [] t = t
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   124
        | mk_abs ((a,T)::Ts) t = Abs (a, T, mk_abs Ts t);
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   125
      val tt = cterm_of sign (mk_abs (params @ [(s, T)]) subt);
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   126
      val Pt = cterm_of sign (mk_abs (params @ [(s, fastype_of1 (T::parTs, subt))])
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   127
                     (make_term t [] paths 0));
8411
d30df828a974 Type.typ_match now uses Vartab instead of association lists.
berghofe
parents: 7652
diff changeset
   128
      val tye = Type.typ_match tsig (Vartab.empty, (tT, #T (rep_cterm tt)));
d30df828a974 Type.typ_match now uses Vartab instead of association lists.
berghofe
parents: 7652
diff changeset
   129
      val tye' = Vartab.dest (Type.typ_match tsig (tye, (PT, #T (rep_cterm Pt))));
3655
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   130
      val ctye = map (fn (x, y) => (x, ctyp_of sign y)) tye';
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   131
      val tv = cterm_of sign (Var (("t", j), typ_subst_TVars tye' tT));
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   132
      val Pv = cterm_of sign (Var (("P", j), typ_subst_TVars tye' PT));
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   133
      val rule' = instantiate (ctye, [(tv, tt), (Pv, Pt)]) rule
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   134
  in rule' end;
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   135
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   136
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   137
(*** extract subgoal i from proof state ***)
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   138
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   139
fun nth_subgoal i thm = nth_elem (i-1, prems_of thm);
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   140
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   141
8411
d30df828a974 Type.typ_match now uses Vartab instead of association lists.
berghofe
parents: 7652
diff changeset
   142
(*** the admissibility tactic ***)
3655
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   143
4039
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
   144
fun try_dest_adm (Const _ $ (Const (name, _) $ Abs abs)) =
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
   145
      if name = adm_name then Some abs else None
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
   146
  | try_dest_adm _ = None;
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
   147
3655
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   148
fun adm_tac tac i state =
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   149
  state |>
4039
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
   150
  let val goali = nth_subgoal i state in
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
   151
    (case try_dest_adm (Logic.strip_assums_concl goali) of
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
   152
      None => no_tac
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
   153
    | Some (s, T, t) =>
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
   154
        let
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
   155
          val sign = sign_of_thm state;
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
   156
          val prems = Logic.strip_assums_hyp goali;
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
   157
          val params = Logic.strip_params goali;
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
   158
          val ts = find_subterms t 0 [];
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
   159
          val ts' = filter eq_terms ts;
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
   160
          val ts'' = filter (is_chfin sign T params) ts';
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
   161
          val thms = foldl (prove_cont tac sign s T prems params) ([], ts'');
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
   162
        in
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
   163
          (case thms of
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
   164
            ((ts as ((t', _)::_), cont_thm)::_) =>
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
   165
              let
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
   166
                val paths = map snd ts;
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
   167
                val rule = inst_adm_subst_thm state i params s T t' t paths;
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
   168
              in
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
   169
                compose_tac (false, rule, 2) i THEN
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
   170
                rtac cont_thm i THEN
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
   171
                REPEAT (assume_tac i) THEN
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4039
diff changeset
   172
                rtac adm_chfin i
4039
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
   173
              end 
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
   174
          | [] => no_tac)
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
   175
        end)
3655
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   176
    end;
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   177
4039
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
   178
3655
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   179
end;
0531f2c64c91 new extended adm tactic introduced;
mueller
parents:
diff changeset
   180
4039
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
   181
0db9f1098fd6 fixed try_dest_adm;
wenzelm
parents: 4005
diff changeset
   182
open Adm;