src/ZF/intr_elim.ML
author lcp
Mon, 27 Feb 1995 17:44:43 +0100
changeset 909 5de21942d046
parent 726 d703d1a1a2af
child 1418 f5f97ee67cbb
permissions -rw-r--r--
intro_tacsf now includes subsetI as an introduction rule. It is needed for rules like list_into_univ
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents: 543
diff changeset
     1
(*  Title: 	ZF/intr_elim.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
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
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
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*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
  val monos      : thm list		(*monotonicity of each M operator*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
  val con_defs   : thm list		(*definitions of the constructors*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
  val type_intrs : thm list		(*type-checking intro rules*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
  val type_elims : thm list		(*type-checking elim rules*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    18
(*internal items*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    19
signature INDUCTIVE_I =
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    20
  sig
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    21
  val rec_tms    : term list		(*the recursive sets*)
726
d703d1a1a2af ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents: 652
diff changeset
    22
  val dom_sum    : term			(*their common domain*)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    23
  val intr_tms   : term list		(*terms for the introduction rules*)
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*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
  val defs	 : thm list		(*definitions made in thy*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
  val bnd_mono   : thm			(*monotonicity for the lfp definition*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
  val unfold     : thm			(*fixed-point equation*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
  val dom_subset : thm			(*inclusion of recursive set in dom*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
  val intrs      : thm list		(*introduction rules*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
  val elim       : thm			(*case analysis theorem*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
  val raw_induct : thm			(*raw induction rule from Fp.induct*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
  val mk_cases : thm list -> string -> thm	(*generates case theorems*)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    37
  val rec_names  : string list		(*names of recursive sets*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
  val sumprod_free_SEs : thm list       (*destruct rules for Su and Pr*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    41
(*prove intr/elim rules for a fixedpoint definition*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    42
functor Intr_elim_Fun
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    43
    (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end  
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    44
     and Fp: FP and Pr : PR and Su : SU) : INTR_ELIM =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
struct
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    46
open Logic Inductive Ind_Syntax;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    48
val rec_names = map (#1 o dest_Const o head_of) rec_tms;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
val big_rec_name = space_implode "_" rec_names;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents: 543
diff changeset
    51
val _ = deny (big_rec_name  mem  map ! (stamps_of_thy thy))
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents: 543
diff changeset
    52
             ("Definition " ^ big_rec_name ^ 
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents: 543
diff changeset
    53
	      " would clash with the theory of the same name!");
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents: 543
diff changeset
    54
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    55
(*fetch fp definitions from the theory*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    56
val big_rec_def::part_rec_defs = 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    57
  map (get_def thy)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    58
      (case rec_names of [_] => rec_names | _ => big_rec_name::rec_names);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    61
val sign = sign_of thy;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
(********)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    64
val _ = writeln "  Proving monotonicity...";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    65
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    66
val Const("==",_) $ _ $ (_ $ dom_sum $ fp_abs) =
543
e961b2092869 ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents: 516
diff changeset
    67
    big_rec_def |> rep_thm |> #prop |> Logic.unvarify;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
val bnd_mono = 
543
e961b2092869 ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents: 516
diff changeset
    70
    prove_goalw_cterm [] 
e961b2092869 ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents: 516
diff changeset
    71
      (cterm_of sign (mk_tprop (Fp.bnd_mono $ dom_sum $ fp_abs)))
e961b2092869 ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents: 516
diff changeset
    72
      (fn _ =>
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
       [rtac (Collect_subset RS bnd_monoI) 1,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
	REPEAT (ares_tac (basic_monos @ monos) 1)]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
val dom_subset = standard (big_rec_def RS Fp.subs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
726
d703d1a1a2af ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents: 652
diff changeset
    78
val unfold = standard ([big_rec_def, bnd_mono] MRS Fp.Tarski);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
(********)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
    81
val _ = writeln "  Proving the introduction rules...";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
726
d703d1a1a2af ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents: 652
diff changeset
    83
(*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
    84
val Part_trans =
d703d1a1a2af ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents: 652
diff changeset
    85
    case rec_names of
d703d1a1a2af ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents: 652
diff changeset
    86
         [_] => asm_rl
d703d1a1a2af ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents: 652
diff changeset
    87
       | _   => standard (Part_subset RS subset_trans);
d703d1a1a2af ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents: 652
diff changeset
    88
d703d1a1a2af ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents: 652
diff changeset
    89
(*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
    90
  enclosed in some monotonic operator M.*)
d703d1a1a2af ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents: 652
diff changeset
    91
val rec_typechecks = 
d703d1a1a2af ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents: 652
diff changeset
    92
   [dom_subset] RL (asm_rl :: ([Part_trans] RL monos)) RL [subsetD];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
(*Type-checking is hardest aspect of proof;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
  disjIn selects the correct disjunct after unfolding*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
fun intro_tacsf disjIn prems = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
  [(*insert prems and underlying sets*)
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 25
diff changeset
    98
   cut_facts_tac prems 1,
726
d703d1a1a2af ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents: 652
diff changeset
    99
   DETERM (rtac (unfold RS ssubst) 1),
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
   REPEAT (resolve_tac [Part_eqI,CollectI] 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
   (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
   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
   103
   (*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
   104
     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
   105
   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
   106
   (*Now solve the equations like Tcons(a,f) = Inl(?b4)*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
   rewrite_goals_tac con_defs,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
   REPEAT (rtac refl 2),
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents: 543
diff changeset
   109
   (*Typechecking; this can fail*)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
   110
   REPEAT (FIRSTGOAL (        dresolve_tac rec_typechecks
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
   111
		      ORELSE' eresolve_tac (asm_rl::PartE::SigmaE2::type_elims)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
   112
		      ORELSE' hyp_subst_tac)),
909
5de21942d046 intro_tacsf now includes subsetI as an introduction rule. It is
lcp
parents: 726
diff changeset
   113
   DEPTH_SOLVE (swap_res_tac (SigmaI::subsetI::type_intrs) 1)];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
(*combines disjI1 and disjI2 to access the corresponding nested disjunct...*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
val mk_disj_rls = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
    let fun f rl = rl RS disjI1
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
   118
	and g rl = rl RS disjI2
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
    in  accesses_bal(f, g, asm_rl)  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
543
e961b2092869 ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents: 516
diff changeset
   121
val intrs = map (uncurry (prove_goalw_cterm part_rec_defs))
e961b2092869 ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents: 516
diff changeset
   122
            (map (cterm_of sign) intr_tms ~~ 
e961b2092869 ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents: 516
diff changeset
   123
	     map intro_tacsf (mk_disj_rls(length intr_tms)));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
(********)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
   126
val _ = writeln "  Proving the elimination rule...";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 25
diff changeset
   128
(*Includes rules for succ and Pair since they are common constructions*)
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 25
diff changeset
   129
val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0, 
652
ff4d4d7fcb7f ZF/intr_elim/elim_rls: now includes Pair_inject, since coinductive
lcp
parents: 634
diff changeset
   130
		Pair_neq_0, sym RS Pair_neq_0, Pair_inject,
ff4d4d7fcb7f ZF/intr_elim/elim_rls: now includes Pair_inject, since coinductive
lcp
parents: 634
diff changeset
   131
		make_elim succ_inject, 
70
8a29f8b4aca1 ZF/ind-syntax/fold_con_tac: deleted, since fold_tac now works
lcp
parents: 55
diff changeset
   132
		refl_thin, conjE, exE, disjE];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
652
ff4d4d7fcb7f ZF/intr_elim/elim_rls: now includes Pair_inject, since coinductive
lcp
parents: 634
diff changeset
   134
(*Standard sum/products for datatypes, variant ones for codatatypes;
ff4d4d7fcb7f ZF/intr_elim/elim_rls: now includes Pair_inject, since coinductive
lcp
parents: 634
diff changeset
   135
  We always include Pair_inject above*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
val sumprod_free_SEs = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
    map (gen_make_elim [conjE,FalseE])
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
   138
	([Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff] 
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
	 RL [iffD1]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
(*Breaks down logical connectives in the monotonic function*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
val basic_elim_tac =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
    REPEAT (SOMEGOAL (eresolve_tac (elim_rls@sumprod_free_SEs)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
   144
	      ORELSE' bound_hyp_subst_tac))
726
d703d1a1a2af ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents: 652
diff changeset
   145
    THEN prune_params_tac
d703d1a1a2af ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents: 652
diff changeset
   146
        (*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
   147
    THEN fold_tac part_rec_defs;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
val elim = rule_by_tactic basic_elim_tac (unfold RS equals_CollectD);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 0
diff changeset
   151
(*Applies freeness of the given constructors, which *must* be unfolded by
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 0
diff changeset
   152
  the given defs.  Cannot simply use the local con_defs because con_defs=[] 
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 0
diff changeset
   153
  for inference systems. *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
fun con_elim_tac defs =
70
8a29f8b4aca1 ZF/ind-syntax/fold_con_tac: deleted, since fold_tac now works
lcp
parents: 55
diff changeset
   155
    rewrite_goals_tac defs THEN basic_elim_tac THEN fold_tac defs;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
(*String s should have the form t:Si where Si is an inductive set*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
fun mk_cases defs s = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
    rule_by_tactic (con_elim_tac defs)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
      (assume_read thy s  RS  elim);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
726
d703d1a1a2af ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents: 652
diff changeset
   162
val defs = big_rec_def :: part_rec_defs;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct);
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 495
diff changeset
   165
end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166