src/ZF/intr_elim.ML
author paulson
Fri, 16 Feb 1996 18:00:47 +0100
changeset 1512 ce37c64244c0
parent 1461 6bcb44e4d6e5
child 2033 639de962ded4
permissions -rw-r--r--
Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1427
diff changeset
     1
(*  Title:      ZF/intr_elim.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1427
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
     4
    Copyright   1994  University of Cambridge
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Introduction/elimination rule module -- for Inductive/Coinductive Definitions
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1427
diff changeset
     9
signature INDUCTIVE_ARG =       (** Description of a (co)inductive def **)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
  sig
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    11
  val thy        : theory               (*new theory with inductive defs*)
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1427
diff changeset
    12
  val monos      : thm list             (*monotonicity of each M operator*)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1427
diff changeset
    13
  val con_defs   : thm list             (*definitions of the constructors*)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1427
diff changeset
    14
  val type_intrs : thm list             (*type-checking intro rules*)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1427
diff changeset
    15
  val type_elims : thm list             (*type-checking elim rules*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 909
diff changeset
    18
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1427
diff changeset
    19
signature INDUCTIVE_I =         (** Terms read from the theory section **)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    20
  sig
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1427
diff changeset
    21
  val rec_tms    : term list            (*the recursive sets*)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1427
diff changeset
    22
  val dom_sum    : term                 (*their common domain*)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1427
diff changeset
    23
  val intr_tms   : term list            (*terms for the introduction rules*)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    24
  end;
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    25
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
signature INTR_ELIM =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
  sig
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    28
  val thy        : theory               (*copy of input theory*)
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1427
diff changeset
    29
  val defs       : thm list             (*definitions made in thy*)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1427
diff changeset
    30
  val bnd_mono   : thm                  (*monotonicity for the lfp definition*)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1427
diff changeset
    31
  val dom_subset : thm                  (*inclusion of recursive set in dom*)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1427
diff changeset
    32
  val intrs      : thm list             (*introduction rules*)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1427
diff changeset
    33
  val elim       : thm                  (*case analysis theorem*)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1427
diff changeset
    34
  val mk_cases   : thm list -> string -> thm    (*generates case theorems*)
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 909
diff changeset
    35
  end;
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 909
diff changeset
    36
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1427
diff changeset
    37
signature INTR_ELIM_AUX =       (** Used to make induction rules **)
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 909
diff changeset
    38
  sig
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1427
diff changeset
    39
  val raw_induct : thm                  (*raw induction rule from Fp.induct*)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1427
diff changeset
    40
  val rec_names  : string list          (*names of recursive sets*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    43
(*prove intr/elim rules for a fixedpoint definition*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    44
functor Intr_elim_Fun
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    45
    (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end  
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 909
diff changeset
    46
     and Fp: FP and Pr : PR and Su : SU) 
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 909
diff changeset
    47
    : sig include INTR_ELIM INTR_ELIM_AUX end =
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 909
diff changeset
    48
let
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 909
diff changeset
    50
val rec_names = map (#1 o dest_Const o head_of) Inductive.rec_tms;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
val big_rec_name = space_implode "_" rec_names;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 909
diff changeset
    53
val _ = deny (big_rec_name  mem  map ! (stamps_of_thy Inductive.thy))
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents: 543
diff changeset
    54
             ("Definition " ^ big_rec_name ^ 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1427
diff changeset
    55
              " would clash with the theory of the same name!");
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents: 543
diff changeset
    56
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    57
(*fetch fp definitions from the theory*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    58
val big_rec_def::part_rec_defs = 
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 909
diff changeset
    59
  map (get_def Inductive.thy)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    60
      (case rec_names of [_] => rec_names | _ => big_rec_name::rec_names);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 909
diff changeset
    63
val sign = sign_of Inductive.thy;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
(********)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    66
val _ = writeln "  Proving monotonicity...";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    67
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    68
val Const("==",_) $ _ $ (_ $ dom_sum $ fp_abs) =
543
e961b2092869 ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents: 516
diff changeset
    69
    big_rec_def |> rep_thm |> #prop |> Logic.unvarify;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
val bnd_mono = 
543
e961b2092869 ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents: 516
diff changeset
    72
    prove_goalw_cterm [] 
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 909
diff changeset
    73
      (cterm_of sign (Ind_Syntax.mk_tprop (Fp.bnd_mono $ dom_sum $ fp_abs)))
543
e961b2092869 ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents: 516
diff changeset
    74
      (fn _ =>
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
       [rtac (Collect_subset RS bnd_monoI) 1,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1427
diff changeset
    76
        REPEAT (ares_tac (basic_monos @ Inductive.monos) 1)]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
val dom_subset = standard (big_rec_def RS Fp.subs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
726
d703d1a1a2af ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents: 652
diff changeset
    80
val unfold = standard ([big_rec_def, bnd_mono] MRS Fp.Tarski);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
(********)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    83
val _ = writeln "  Proving the introduction rules...";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
726
d703d1a1a2af ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents: 652
diff changeset
    85
(*Mutual recursion?  Helps to derive subset rules for the individual sets.*)
d703d1a1a2af ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents: 652
diff changeset
    86
val Part_trans =
d703d1a1a2af ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents: 652
diff changeset
    87
    case rec_names of
d703d1a1a2af ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents: 652
diff changeset
    88
         [_] => asm_rl
d703d1a1a2af ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents: 652
diff changeset
    89
       | _   => standard (Part_subset RS subset_trans);
d703d1a1a2af ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents: 652
diff changeset
    90
d703d1a1a2af ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents: 652
diff changeset
    91
(*To type-check recursive occurrences of the inductive sets, possibly
d703d1a1a2af ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents: 652
diff changeset
    92
  enclosed in some monotonic operator M.*)
d703d1a1a2af ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents: 652
diff changeset
    93
val rec_typechecks = 
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 909
diff changeset
    94
   [dom_subset] RL (asm_rl :: ([Part_trans] RL Inductive.monos)) RL [subsetD];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
(*Type-checking is hardest aspect of proof;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
  disjIn selects the correct disjunct after unfolding*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
fun intro_tacsf disjIn prems = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
  [(*insert prems and underlying sets*)
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 25
diff changeset
   100
   cut_facts_tac prems 1,
726
d703d1a1a2af ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents: 652
diff changeset
   101
   DETERM (rtac (unfold RS ssubst) 1),
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
   REPEAT (resolve_tac [Part_eqI,CollectI] 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
   (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
   rtac disjIn 2,
634
8a5f6961250f {HOL,ZF}/intr_elim/intro_tacsf: now calls DEPTH_SOLVE_1 instead of REPEAT to
lcp
parents: 590
diff changeset
   105
   (*Not ares_tac, since refl must be tried before any equality assumptions;
8a5f6961250f {HOL,ZF}/intr_elim/intro_tacsf: now calls DEPTH_SOLVE_1 instead of REPEAT to
lcp
parents: 590
diff changeset
   106
     backtracking may occur if the premises have extra variables!*)
8a5f6961250f {HOL,ZF}/intr_elim/intro_tacsf: now calls DEPTH_SOLVE_1 instead of REPEAT to
lcp
parents: 590
diff changeset
   107
   DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 2 ORELSE assume_tac 2),
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents: 543
diff changeset
   108
   (*Now solve the equations like Tcons(a,f) = Inl(?b4)*)
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 909
diff changeset
   109
   rewrite_goals_tac Inductive.con_defs,
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
   REPEAT (rtac refl 2),
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents: 543
diff changeset
   111
   (*Typechecking; this can fail*)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
   112
   REPEAT (FIRSTGOAL (        dresolve_tac rec_typechecks
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1427
diff changeset
   113
                      ORELSE' eresolve_tac (asm_rl::PartE::SigmaE2::
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1427
diff changeset
   114
                                            Inductive.type_elims)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1427
diff changeset
   115
                      ORELSE' hyp_subst_tac)),
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 909
diff changeset
   116
   DEPTH_SOLVE (swap_res_tac (SigmaI::subsetI::Inductive.type_intrs) 1)];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
(*combines disjI1 and disjI2 to access the corresponding nested disjunct...*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
val mk_disj_rls = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
    let fun f rl = rl RS disjI1
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1427
diff changeset
   121
        and g rl = rl RS disjI2
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
    in  accesses_bal(f, g, asm_rl)  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
543
e961b2092869 ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents: 516
diff changeset
   124
val intrs = map (uncurry (prove_goalw_cterm part_rec_defs))
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 909
diff changeset
   125
            (map (cterm_of sign) Inductive.intr_tms ~~ 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1427
diff changeset
   126
             map intro_tacsf (mk_disj_rls(length Inductive.intr_tms)));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
(********)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
   129
val _ = writeln "  Proving the elimination rule...";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
(*Breaks down logical connectives in the monotonic function*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
val basic_elim_tac =
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 909
diff changeset
   133
    REPEAT (SOMEGOAL (eresolve_tac (Ind_Syntax.elim_rls @ Su.free_SEs)
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1427
diff changeset
   134
              ORELSE' bound_hyp_subst_tac))
726
d703d1a1a2af ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents: 652
diff changeset
   135
    THEN prune_params_tac
d703d1a1a2af ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents: 652
diff changeset
   136
        (*Mutual recursion: collapse references to Part(D,h)*)
d703d1a1a2af ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents: 652
diff changeset
   137
    THEN fold_tac part_rec_defs;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 909
diff changeset
   139
in
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 909
diff changeset
   140
  struct
1427
ecd90b82ab8e Purely cosmetic changes
paulson
parents: 1418
diff changeset
   141
  val thy = Inductive.thy
ecd90b82ab8e Purely cosmetic changes
paulson
parents: 1418
diff changeset
   142
  and defs = big_rec_def :: part_rec_defs
ecd90b82ab8e Purely cosmetic changes
paulson
parents: 1418
diff changeset
   143
  and bnd_mono   = bnd_mono
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 909
diff changeset
   144
  and dom_subset = dom_subset
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 909
diff changeset
   145
  and intrs      = intrs;
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 909
diff changeset
   146
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 909
diff changeset
   147
  val elim = rule_by_tactic basic_elim_tac 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1427
diff changeset
   148
                  (unfold RS Ind_Syntax.equals_CollectD);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 909
diff changeset
   150
  (*Applies freeness of the given constructors, which *must* be unfolded by
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 909
diff changeset
   151
      the given defs.  Cannot simply use the local con_defs because  
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 909
diff changeset
   152
      con_defs=[] for inference systems. 
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 909
diff changeset
   153
    String s should have the form t:Si where Si is an inductive set*)
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 909
diff changeset
   154
  fun mk_cases defs s = 
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 909
diff changeset
   155
      rule_by_tactic (rewrite_goals_tac defs THEN 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1427
diff changeset
   156
                      basic_elim_tac THEN
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1427
diff changeset
   157
                      fold_tac defs)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1427
diff changeset
   158
        (assume_read Inductive.thy s  RS  elim);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
1427
ecd90b82ab8e Purely cosmetic changes
paulson
parents: 1418
diff changeset
   160
  val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct)
ecd90b82ab8e Purely cosmetic changes
paulson
parents: 1418
diff changeset
   161
  and rec_names = rec_names
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 909
diff changeset
   162
  end
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
   163
end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164