src/HOLCF/Tools/adm_tac.ML
author paulson
Fri, 05 Oct 2007 09:59:03 +0200
changeset 24854 0ebcd575d3c6
parent 23152 9497234a2743
child 25804 cf41372cfee6
permissions -rw-r--r--
filtering out some package theorems
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     1
(*  ID:         $Id$
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     2
    Author:     Stefan Berghofer, TU Muenchen
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     3
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     4
Admissibility tactic.
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     5
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     6
Checks whether adm_subst theorem is applicable to the current proof
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     7
state:
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     8
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     9
  [| cont t; adm P |] ==> adm (%x. P (t x))
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    10
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    11
"t" is instantiated with a term of chain-finite type, so that
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    12
adm_chfin can be applied:
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    13
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    14
  adm (P::'a::{chfin,pcpo} => bool)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    15
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    16
*)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    17
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    18
signature ADM =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    19
sig
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    20
  val adm_tac: (int -> tactic) -> int -> tactic
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    21
end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    22
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    23
structure Adm: ADM =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    24
struct
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    25
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    26
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    27
(*** find_subterms t 0 []
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    28
     returns lists of terms with the following properties:
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    29
       1. all terms in the list are disjoint subterms of t
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    30
       2. all terms contain the variable which is bound at level 0
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    31
       3. all occurences of the variable which is bound at level 0
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    32
          are "covered" by a term in the list
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    33
     a list of integers is associated with every term which describes
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    34
     the "path" leading to the subterm (required for instantiation of
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    35
     the adm_subst theorem (see functions mk_term, inst_adm_subst_thm))
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    36
***)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    37
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    38
fun find_subterms (Bound i) lev path =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    39
      if i = lev then [[(Bound 0, path)]]
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    40
      else []
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    41
  | find_subterms (t as (Abs (_, _, t2))) lev path =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    42
      if List.filter (fn x => x<=lev)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    43
           (add_loose_bnos (t, 0, [])) = [lev] then
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    44
        [(incr_bv (~lev, 0, t), path)]::
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    45
        (find_subterms t2 (lev+1) (0::path))
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    46
      else find_subterms t2 (lev+1) (0::path)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    47
  | find_subterms (t as (t1 $ t2)) lev path =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    48
      let val ts1 = find_subterms t1 lev (0::path);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    49
          val ts2 = find_subterms t2 lev (1::path);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    50
          fun combine [] y = []
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    51
            | combine (x::xs) ys =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    52
                (map (fn z => x @ z) ys) @ (combine xs ys)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    53
      in
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    54
        (if List.filter (fn x => x<=lev)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    55
              (add_loose_bnos (t, 0, [])) = [lev] then
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    56
           [[(incr_bv (~lev, 0, t), path)]]
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    57
         else []) @
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    58
        (if ts1 = [] then ts2
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    59
         else if ts2 = [] then ts1
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    60
         else combine ts1 ts2)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    61
      end
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    62
  | find_subterms _ _ _ = [];
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    63
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    64
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    65
(*** make term for instantiation of predicate "P" in adm_subst theorem ***)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    66
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    67
fun make_term t path paths lev =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    68
  if path mem paths then Bound lev
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    69
  else case t of
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    70
      (Abs (s, T, t1)) => Abs (s, T, make_term t1 (0::path) paths (lev+1))
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    71
    | (t1 $ t2) => (make_term t1 (0::path) paths lev) $
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    72
                   (make_term t2 (1::path) paths lev)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    73
    | t1 => t1;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    74
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    75
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    76
(*** check whether all terms in list are equal ***)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    77
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    78
fun eq_terms [] = true
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    79
  | eq_terms (ts as (t, _) :: _) = forall (fn (t2, _) => t2 aconv t) ts;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    80
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    81
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    82
(*figure out internal names*)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    83
val chfin_pcpoS = Sign.intern_sort (the_context ()) ["chfin", "pcpo"];
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    84
val cont_name = Sign.intern_const (the_context ()) "cont";
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    85
val adm_name = Sign.intern_const (the_context ()) "adm";
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    86
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    87
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    88
(*** check whether type of terms in list is chain finite ***)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    89
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    90
fun is_chfin sign T params ((t, _)::_) =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    91
  let val parTs = map snd (rev params)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    92
  in Sign.of_sort sign (fastype_of1 (T::parTs, t), chfin_pcpoS) end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    93
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    94
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    95
(*** try to prove that terms in list are continuous
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    96
     if successful, add continuity theorem to list l ***)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    97
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    98
fun prove_cont tac sign s T prems params (l, ts as ((t, _)::_)) =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    99
  let val parTs = map snd (rev params);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   100
       val contT = (T --> (fastype_of1 (T::parTs, t))) --> HOLogic.boolT;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   101
       fun mk_all [] t = t
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   102
         | mk_all ((a,T)::Ts) t = (all T) $ (Abs (a, T, mk_all Ts t));
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   103
       val t = HOLogic.mk_Trueprop((Const (cont_name, contT)) $ (Abs(s, T, t)));
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   104
       val t' = mk_all params (Logic.list_implies (prems, t));
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   105
       val thm = Goal.prove (ProofContext.init sign) [] [] t' (K (tac 1));
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   106
  in (ts, thm)::l end
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   107
  handle ERROR _ => l;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   108
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   109
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   110
(*** instantiation of adm_subst theorem (a bit tricky) ***)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   111
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   112
fun inst_adm_subst_thm state i params s T subt t paths =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   113
  let val {thy = sign, maxidx, ...} = rep_thm state;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   114
      val j = maxidx+1;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   115
      val parTs = map snd (rev params);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   116
      val rule = Thm.lift_rule (Thm.cprem_of state i) adm_subst;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   117
      val types = valOf o (fst (types_sorts rule));
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   118
      val tT = types ("t", j);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   119
      val PT = types ("P", j);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   120
      fun mk_abs [] t = t
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   121
        | mk_abs ((a,T)::Ts) t = Abs (a, T, mk_abs Ts t);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   122
      val tt = cterm_of sign (mk_abs (params @ [(s, T)]) subt);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   123
      val Pt = cterm_of sign (mk_abs (params @ [(s, fastype_of1 (T::parTs, subt))])
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   124
                     (make_term t [] paths 0));
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   125
      val tye = Sign.typ_match sign (tT, #T (rep_cterm tt)) Vartab.empty;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   126
      val tye' = Sign.typ_match sign (PT, #T (rep_cterm Pt)) tye;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   127
      val ctye = map (fn (ixn, (S, T)) =>
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   128
        (ctyp_of sign (TVar (ixn, S)), ctyp_of sign T)) (Vartab.dest tye');
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   129
      val tv = cterm_of sign (Var (("t", j), Envir.typ_subst_TVars tye' tT));
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   130
      val Pv = cterm_of sign (Var (("P", j), Envir.typ_subst_TVars tye' PT));
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   131
      val rule' = instantiate (ctye, [(tv, tt), (Pv, Pt)]) rule
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   132
  in rule' end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   133
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   134
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   135
(*** extract subgoal i from proof state ***)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   136
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   137
fun nth_subgoal i thm = List.nth (prems_of thm, i-1);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   138
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   139
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   140
(*** the admissibility tactic ***)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   141
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   142
fun try_dest_adm (Const _ $ (Const (name, _) $ Abs abs)) =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   143
      if name = adm_name then SOME abs else NONE
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   144
  | try_dest_adm _ = NONE;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   145
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   146
fun adm_tac tac i state =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   147
  state |>
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   148
  let val goali = nth_subgoal i state in
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   149
    (case try_dest_adm (Logic.strip_assums_concl goali) of
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   150
      NONE => no_tac
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   151
    | SOME (s, T, t) =>
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   152
        let
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   153
          val sign = Thm.theory_of_thm state;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   154
          val prems = Logic.strip_assums_hyp goali;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   155
          val params = Logic.strip_params goali;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   156
          val ts = find_subterms t 0 [];
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   157
          val ts' = List.filter eq_terms ts;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   158
          val ts'' = List.filter (is_chfin sign T params) ts';
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   159
          val thms = Library.foldl (prove_cont tac sign s T prems params) ([], ts'');
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   160
        in
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   161
          (case thms of
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   162
            ((ts as ((t', _)::_), cont_thm)::_) =>
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   163
              let
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   164
                val paths = map snd ts;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   165
                val rule = inst_adm_subst_thm state i params s T t' t paths;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   166
              in
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   167
                compose_tac (false, rule, 2) i THEN
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   168
                rtac cont_thm i THEN
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   169
                REPEAT (assume_tac i) THEN
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   170
                rtac adm_chfin i
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   171
              end 
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   172
          | [] => no_tac)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   173
        end)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   174
    end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   175
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   176
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   177
end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   178
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   179
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   180
open Adm;