isabelle-cookbook: comparison ProgTutorial/Package/Ind

equal deleted inserted replaced

-:069d525f8f1d
+:ca0ac2e75f6d
 expanding the defs, gives
 @{text [display]
 "\<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> (\<forall>preds. orules \<longrightarrow> pred ss))\<^isup>* \<longrightarrow>  (\<forall>preds. orules \<longrightarrow> pred ts"}
-applying as many allI and impI as possible
+By applying as many allI and impI as possible, we have
-so we have @{text "As"}, @{text "(\<forall>ys. Bs \<longrightarrow> (\<forall>preds. orules \<longrightarrow> pred ss))\<^isup>*"},
+@{text "As"}, @{text "(\<forall>ys. Bs \<longrightarrow> (\<forall>preds. orules \<longrightarrow> pred ss))\<^isup>*"},
 @{text "orules"}; and have to show @{text "pred ts"}
 the $i$th @{text "orule"} is of the
 form @{text "\<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"}.
-using the @{text "As"} we ????
+So we apply the $i$th @{text "orule"}, but we have to show the @{text "As"} (by assumption)
-*}
+and all @{text "(\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>*"}. For the latter we use the assumptions
+@{text "(\<forall>ys. Bs \<longrightarrow> (\<forall>preds. orules \<longrightarrow> pred ss))\<^isup>*"} and @{text "orules"}.
-text {*
+*}
-First we have to produce for each predicate its definitions of the form
+text {*
+First we have to produce for each predicate the definition of the form
 @{text [display] "pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}
-In order to make definitions, we use the following wrapper for
+and then ``register'' the definitions with Isabelle.
+To do the latter, we use the following wrapper for
 @{ML LocalTheory.define}. The wrapper takes a predicate name, a syntax
 annotation and a term representing the right-hand side of the definition.
 *}
 ML %linenosgray{*fun make_defs ((predname, syn), trm) lthy =
 \begin{isabelle}
 \isacommand{thm}~@{text "MyTrue_def"}\\
 @{text "> MyTrue \<equiv> True"}
 \end{isabelle}
-The next two functions construct the terms we need for the definitions for
+The next two functions construct the right-hand sides of the definitions, which
-our \isacommand{simple\_inductive} command. These
+are of the form
-terms are of the form
+@{text [display] "\<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}
-@{text [display] "\<lambda>\<^raw:$zs$>. \<forall>preds. orules \<longrightarrow> pred \<^raw:$zs$>"}
+The variables @{text "zs"} need to be chosen so that they do not occur
-The variables @{text "\<^raw:$zs$>"} need to be chosen so that they do not occur
 in the @{text orules} and also be distinct from the @{text "preds"}.
 The first function constructs the term for one particular predicate, say
 @{text "pred"}; the number of arguments of this predicate is
-determined by the number of argument types of @{text "arg_tys"}.
+determined by the number of argument types given in @{text "arg_tys"}.
-So it takes these two parameters as arguments. The other arguments are
+The other arguments are all @{text "preds"} and the @{text "orules"}.
-all the @{text "preds"} and the @{text "orules"}.
 *}
 ML %linenosgray{*fun defs_aux lthy orules preds (pred, arg_tys) =
 let
 fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P
 end*}
 text {*
 The function in Line 3 is just a helper function for constructing universal
 quantifications. The code in Lines 5 to 9 produces the fresh @{text
-"\<^raw:$zs$>"}. For this it pairs every argument type with the string
+"zs"}. For this it pairs every argument type with the string
 @{text [quotes] "z"} (Line 7); then generates variants for all these strings
-so that they are unique w.r.t.~to the @{text "orules"} and the predicates;
+so that they are unique w.r.t.~to the predicates and @{text "orules"} (Line 8);
 in Line 9 it generates the corresponding variable terms for the unique
 strings.
 The unique free variables are applied to the predicate (Line 11) using the
 function @{ML list_comb}; then the @{text orules} are prefixed (Line 12); in
 Line 13 we quantify over all predicates; and in line 14 we just abstract
-over all the @{text "\<^raw:$zs$>"}, i.e.~the fresh arguments of the
+over all the @{text "zs"}, i.e.~the fresh arguments of the
-predicate.
+predicate. A testcase for this function is
-A testcase for this function is
 *}
 local_setup %gray{* fn lthy =>
 let
 val orules = [@{prop "even 0"},
 @{prop "\<forall>n::nat. odd n \<longrightarrow> even (Suc n)"},
 @{prop "\<forall>n::nat. even n \<longrightarrow> odd (Suc n)"}]
-val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}, @{term "z::nat"}]
+val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
 val pred = @{term "even::nat\<Rightarrow>bool"}
 val arg_tys = [@{typ "nat"}]
 val def = defs_aux lthy orules preds (pred, arg_tys)
 in
 warning (Syntax.string_of_term lthy def); lthy
 end *}
 text {*
-It constructs the left-hand side for the definition of @{text "even"}. So we obtain
+It calls @{ML defs_aux} for the definition of @{text "even"} and prints
-as printout the term
+out the definition. So we obtain as printout
 @{text [display]
 "\<lambda>z. \<forall>even odd. (even 0) \<longrightarrow> (\<forall>n. odd n \<longrightarrow> even (Suc n))
 \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> even z"}
-The main function for the definitions now has to just iterate the function
+The second function for the definitions has to just iterate the function
 @{ML defs_aux} over all predicates. The argument @{text "preds"} is again
 the the list of predicates as @{ML_type term}s; the argument @{text
 "prednames"} is the list of names of the predicates; @{text "arg_tyss"} is
 the list of argument-type-lists for each predicate.
 *}
 meta-connectives). To do this transformation we have to obtain the theory
 behind the local theory (Line 3); with this theory we can use the function
 @{ML ObjectLogic.atomize_term} to make the transformation (Line 4). The call
 to @{ML defs_aux} in Line 5 produces all left-hand sides of the
 definitions. The actual definitions are then made in Line 7.  The result
-of the function is a list of theorems and a local theory.
+of the function is a list of theorems and a local theory. A testcase for
+this function is
-A testcase for this function is
 *}
 local_setup %gray {* fn lthy =>
 let
 val rules = [@{prop "even 0"},
 apply(drule spec[where x=Q])
 apply(assumption)
 done
 text {*
-The code for such induction principles has to accomplish two tasks:
+The code for automating such induction principles has to accomplish two tasks:
 constructing the induction principles from the given introduction
-rules and then automatically generating a proof of them using a tactic.
+rules and then automatically generating proofs for them using a tactic.
 The tactic will use the following helper function for instantiating universal
 quantifiers.
 *}
 ML{*fun inst_spec_tac ctrms =
 EVERY' (map (dtac o inst_spec) ctrms)*}
 text {*
-we can use @{ML inst_spec} in the following proof to instantiate the
+we can use @{ML inst_spec_tac} in the following proof to instantiate the
 three quantifiers in the assumption.
 *}
 lemma
 fixes P::"nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
 K (rewrite_goals_tac defs),
 inst_spec_tac insts,
 assume_tac]*}
 text {*
-We only have to give it as arguments the definitions, the premise
+We only have to give it the definitions, the premise (like @{text "even n"})
-(like @{text "even n"})
+and the instantiations as arguments. Compare this with the manual proof
-and the instantiations. Compare this with the manual proof given for the
+given for the lemma @{thm [source] man_ind_principle}: there is almos a
-lemma @{thm [source] man_ind_principle}.
+one-to-one correspondence between the \isacommand{apply}-script and the
-A testcase for this tactic is the function
+@{ML induction_tac}. A testcase for this tactic is the function
 *}
 ML{*fun test_tac prems =
 let
 val defs = [@{thm even_def}, @{thm odd_def}]
 text {*
 which indeed proves the induction principle:
 *}
-lemma
+lemma auto_ind_principle:
 assumes prems: "even n"
 shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
 apply(tactic {* test_tac @{thms prems} *})
 done
 it is a bit harder to construct the goals from the introduction
 rules the user provides. In general we have to construct for each predicate
 @{text "pred"} a goal of the form
 @{text [display]
-"\<And>\<^raw:$zs$>. pred \<^raw:$zs$> \<Longrightarrow> rules[preds := \<^raw:$Ps$>] \<Longrightarrow> \<^raw:$P$> \<^raw:$zs$>"}
+"pred ?zs \<Longrightarrow> rules[preds := ?Ps] \<Longrightarrow> ?P$ ?zs"}
-where the given predicates @{text preds} are replaced in the introduction
+where the predicates @{text preds} are replaced in the introduction
-rules by new distinct variables written @{text "\<^raw:$Ps$>"}.
+rules by new distinct variables written @{text "Ps"}.
 We also need to generate fresh arguments for the predicate @{text "pred"} in
-the premise and the @{text "\<^raw:$P$>"} in the conclusion. We achieve
+the premise and the @{text "?P"} in the conclusion. Note
+that the  @{text "?Ps"}  and @{text "?zs"} need to be
+schematic variables that can be instantiated. This corresponds to what the
+@{thm [source] auto_ind_principle} looks like:
+\begin{isabelle}
+\isacommand{thm}~@{thm [source] auto_ind_principle}\\
+@{text "> \<lbrakk>even ?n; ?P 0; \<And>m. ?Q m \<Longrightarrow> ?P (Suc m); \<And>m. ?P m \<Longrightarrow> ?Q (Suc m)\<rbrakk> \<Longrightarrow> ?P ?n"}
+\end{isabelle}
+We achieve
 that in two steps.
 The function below expects that the introduction rules are already appropriately
 substituted. The argument @{text "srules"} stands for these substituted
 rules; @{text cnewpreds} are the certified terms coresponding
-to the variables @{text "\<^raw:$Ps$>"}; @{text "pred"} is the predicate for
+to the variables @{text "Ps"}; @{text "pred"} is the predicate for
 which we prove the introduction principle; @{text "newpred"} is its
 replacement and @{text "tys"} are the argument types of this predicate.
 *}
-ML %linenosgray{*fun prove_induction lthy defs srules cnewpreds ((pred, newpred), tys)  =
+ML %linenosgray{*fun prove_induction lthy defs srules cnewpreds ((pred, newpred), arg_tys)  =
 let
-val zs = replicate (length tys) "z"
+val zs = replicate (length arg_tys) "z"
 val (newargnames, lthy') = Variable.variant_fixes zs lthy;
-val newargs = map Free (newargnames ~~ tys)
+val newargs = map Free (newargnames ~~ arg_tys)
 val prem = HOLogic.mk_Trueprop (list_comb (pred, newargs))
 val goal = Logic.list_implies
 (srules, HOLogic.mk_Trueprop (list_comb (newpred, newargs)))
 in
 (fn {prems, ...} => induction_tac defs prems cnewpreds)
 |> singleton (ProofContext.export lthy' lthy)
 end *}
 text {*
-In Line 3 we produce names @{text "\<^raw:$zs$>"} for each type in the
+In Line 3 we produce names @{text "zs"} for each type in the
 argument type list. Line 4 makes these names unique and declares them as
 \emph{free} (but fixed) variables in the local theory @{text "lthy'"}. In
 Line 5 we just construct the terms corresponding to these variables.
 The term variables are applied to the predicate in Line 7 (this corresponds
-to the first premise @{text "pred \<^raw:$zs$>"} of the induction principle).
+to the first premise @{text "pred zs"} of the induction principle).
-In Line 8 and 9, we first construct the term  @{text "\<^raw:$P$>\<^raw:$zs$>"}
+In Line 8 and 9, we first construct the term  @{text "P zs"}
 and then add the (substituded) introduction rules as premises. In case that
 no introduction rules are given, the conclusion of this implication needs
 to be wrapped inside a @{term Trueprop}, otherwise the Isabelle's goal
 mechanism will fail.
-In Line 11 we set up the goal to be proved; in the next line call the tactic
+In Line 11 we set up the goal to be proved; in the next line we call the tactic
-for proving the induction principle. This tactic expects definitions, the
+for proving the induction principle. This tactic expects the definitions, the
 premise and the (certified) predicates with which the introduction rules
-have been substituted. This will return a theorem. However, it is a theorem
+have been substituted. The code in these two lines will return a theorem.
+However, it is a theorem
 proved inside the local theory @{text "lthy'"}, where the variables @{text
-"\<^raw:$zs$>"} are fixed, but free. By exporting this theorem from @{text
+"zs"} are fixed, but free. By exporting this theorem from @{text
-"lthy'"} (which contains the @{text "\<^raw:$zs$>"} as free) to @{text
+"lthy'"} (which contains the @{text "zs"} as free) to @{text
-"lthy"} (which does not), we obtain the desired quantifications @{text
+"lthy"} (which does not), we obtain the desired schematic variables.
-"\<And>\<^raw:$zs$>"}.
+*}
-(FIXME testcase)
+local_setup %gray{* fn lthy =>
+let
+val defs = [@{thm even_def}, @{thm odd_def}]
-Now it is left to produce the new predicates with which the introduction
+val srules = [@{prop "P (0::nat)"},
-rules are substituted.
+@{prop "\<And>n::nat. Q n \<Longrightarrow> P (Suc n)"},
+@{prop "\<And>n::nat. P n \<Longrightarrow> Q (Suc n)"}]
+val cnewpreds = [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}]
+val pred = @{term "even::nat\<Rightarrow>bool"}
+val newpred = @{term "P::nat\<Rightarrow>bool"}
+val arg_tys = [@{typ "nat"}]
+val intro =
+prove_induction lthy defs srules cnewpreds ((pred, newpred), arg_tys)
+in
+warning (str_of_thm_raw lthy intro); lthy
+end *}
+text {*
+This prints out:
+@{text [display]
+" \<lbrakk>even ?z; P 0; \<And>n. Q n \<Longrightarrow> P (Suc n); \<And>n. P n \<Longrightarrow> Q (Suc n)\<rbrakk> \<Longrightarrow> P ?z"}
+Note that the export from @{text lthy'} to @{text lthy} in Line 13 above
+has turned the free, but fixed, @{text "z"} into a schematic
+variable @{text "?z"}.
+We still have to produce the new predicates with which the introduction
+rules are substituted and iterate @{ML prove_induction} over all
+predicates. This is what the next function does.
 *}
 ML %linenosgray{*fun inductions rules defs preds arg_tyss lthy  =
 let
 val Ps = replicate (length preds) "P"
 end*}
 text {*
 In Line 3 we generate a string @{text [quotes] "P"} for each predicate.
 In Line 4, we use the same trick as in the previous function, that is making the
-@{text "\<^raw:$Ps$>"} fresh and declaring them as fixed but free in
+@{text "Ps"} fresh and declaring them as fixed, but free, in
 the new local theory @{text "lthy'"}. From the local theory we extract
 the ambient theory in Line 6. We need this theory in order to certify
 the new predicates. In Line 8 we calculate the types of these new predicates
-using the argument types. Next we turn them into terms and subsequently
+using the given argument types. Next we turn them into terms and subsequently
-certify them. We can now produce the substituted introduction rules
+certify them (Line 9 and 10). We can now produce the substituted introduction rules
-(Line 11). Line 14 and 15 just iterate the proofs for all predicates.
+(Line 11) using the function @{ML subst_free}. Line 14 and 15 just iterate
+the proofs for all predicates.
 From this we obtain a list of theorems. Finally we need to export the
-fixed variables @{text "\<^raw:$Ps$>"} to obtain the correct quantification
+fixed variables @{text "Ps"} to obtain the schematic variables
 (Line 16).
 A testcase for this function is
 *}
 val defs = [@{thm even_def}, @{thm odd_def}]
 val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
 val tyss = [[@{typ "nat"}], [@{typ "nat"}]]
 val ind_thms = inductions rules defs preds tyss lthy
 in
-warning (str_of_thms lthy ind_thms); lthy
+warning (str_of_thms_raw lthy ind_thms); lthy
-end
+end *}
-*}
 text {*
 which prints out
 @{text [display]
-"> even z \<Longrightarrow>
+"> even ?z \<Longrightarrow> ?P1 0 \<Longrightarrow>
->  P 0 \<Longrightarrow> (\<And>m. Pa m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Pa (Suc m)) \<Longrightarrow> P z,
+> (\<And>m. ?Pa1 m \<Longrightarrow> ?P1 (Suc m)) \<Longrightarrow> (\<And>m. ?P1 m \<Longrightarrow> ?Pa1 (Suc m)) \<Longrightarrow> ?P1 ?z,
-> odd z \<Longrightarrow>
+> odd ?z \<Longrightarrow> ?P1 0
->  P 0 \<Longrightarrow> (\<And>m. Pa m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Pa (Suc m)) \<Longrightarrow> Pa z"}
+> \<Longrightarrow> (\<And>m. ?Pa1 m \<Longrightarrow> ?P1 (Suc m)) \<Longrightarrow> (\<And>m. ?P1 m \<Longrightarrow> ?Pa1 (Suc m)) \<Longrightarrow> ?Pa1 ?z"}
-This completes the code for the induction principles. Finally we can
+Note that now both, the @{text "Ps"} and the @{text "zs"}, are schematic
-prove the introduction rules.
+variables. The numbers have been introduced by the pretty-printer and are
+not significant.
-*}
+This completes the code for the induction principles.  Finally we can prove the
-ML {* ObjectLogic.rulify  *}
+introduction rules. Their proofs are quite a bit more involved. To ease them
+somewhat we  use the following two helper function.
+*}
 ML{*val all_elims = fold (fn ct => fn th => th RS inst_spec ct)
 val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp})*}
+text {*
+To see what they do, let us suppose whe have the follwoing three
+theorems.
+*}
+lemma all_elims_test:
+fixes P::"nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
+shows "\<forall>x y z. P x y z" sorry
+lemma imp_elims_test:
+fixes A B C::"bool"
+shows "A \<longrightarrow> B \<longrightarrow> C" sorry
+lemma imp_elims_test':
+fixes A::"bool"
+shows "A" "B" sorry
+text {*
+The function @{ML all_elims} takes a list of (certified) terms and instantiates
+theorems of the form @{thm [source] all_elims_test}. For example we can instantiate
+the quantifiers in this theorem with @{term a}, @{term b} and @{term c} as follows
+@{ML_response_fake [display, gray]
+"let
+val ctrms = [@{cterm \"a::nat\"}, @{cterm \"b::nat\"}, @{cterm \"c::nat\"}]
+val new_thm = all_elims ctrms @{thm all_elims_test}
+in
+warning (str_of_thm @{context} new_thm)
+end"
+"P a b c"}
+Similarly, the function @{ML imp_elims} eliminates preconditions from implications.
+For example
+@{ML_response_fake [display, gray]
+"warning (str_of_thm @{context}
+(imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}))"
+"C"}
+*}
+ML {* prems_of *}
+ML {* Logic.strip_params *}
+ML {* Logic.strip_assums_hyp *}
+ML {*
+fun chop_print_tac ctxt thm =
+let
+val [trm] = prems_of thm
+val params = map fst (Logic.strip_params trm)
+val prems  = Logic.strip_assums_hyp trm
+val (prems1, prems2) = chop (length prems - 3) prems;
+val (params1, params2) = chop (length params - 2) params;
+val _ = warning (Syntax.string_of_term ctxt trm)
+val _ = warning (commas params)
+val _ = warning (commas (map (Syntax.string_of_term ctxt) prems))
+val _ = warning ((commas params1) ^ " | " ^ (commas params2))
+val _ = warning ((commas (map (Syntax.string_of_term ctxt) prems1)) ^ " | " ^
+(commas (map (Syntax.string_of_term ctxt) prems2)))
+in
+Seq.single thm
+end
+*}
+lemma intro1:
+shows "\<And>m. odd m \<Longrightarrow> even (Suc m)"
+apply(tactic {* ObjectLogic.rulify_tac 1 *})
+apply(tactic {* rewrite_goals_tac [@{thm even_def}, @{thm odd_def}] *})
+apply(tactic {* REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1) *})
+apply(tactic {* chop_print_tac @{context} *})
+oops
 ML{*fun subproof2 prem params2 prems2 =
 SUBPROOF (fn {prems, ...} =>
 let
 val prem' = prems MRS prem;
 | _ => prem';
 in
 rtac prem'' 1
 end)*}
-ML{*fun subproof1 rules preds i =
+text {*
+*}
+ML %linenosgray{*fun subproof1 rules preds i =
 SUBPROOF (fn {params, prems, context = ctxt', ...} =>
 let
 val (prems1, prems2) = chop (length prems - length rules) prems;
 val (params1, params2) = chop (length params - length preds) params;
 in
 rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1
+(* applicateion of the i-ith intro rule *)
 THEN
 EVERY1 (map (fn prem => subproof2 prem params2 prems2 ctxt') prems1)
 end)*}
+text {*
+@{text "params1"} are the variables of the rules; @{text "params2"} is
+the variables corresponding to the @{text "preds"}.
+@{text "prems1"} are the assumption corresponding to the rules;
+@{text "prems2"} are the assumptions coming from the allIs/impIs
+you instantiate the parameters i-th introduction rule with the parameters
+that come from the rule; and you apply it to the goal
+this now generates subgoals corresponding to the premisses of this
+intro rule
+*}
 ML{*
-fun introductions_tac defs rules preds i ctxt =
+fun intros_tac defs rules preds i ctxt =
 EVERY1 [ObjectLogic.rulify_tac,
 K (rewrite_goals_tac defs),
 REPEAT o (resolve_tac [@{thm allI}, @{thm impI}]),
 subproof1 rules preds i ctxt]*}
-lemma evenS:
+text {*
-shows "odd m \<Longrightarrow> even (Suc m)"
+A test case
-apply(tactic {*
+*}
+ML{*fun intros_tac_test ctxt i =
 let
 val rules = [@{prop "even (0::nat)"},
 @{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"},
 @{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}]
 val defs = [@{thm even_def}, @{thm odd_def}]
 val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
 in
-introductions_tac defs rules preds 1 @{context}
+intros_tac defs rules preds i ctxt
-end *})
+end*}
+lemma intro0:
+shows "even 0"
+apply(tactic {* intros_tac_test @{context} 0 *})
+done
+lemma intro1:
+shows "\<And>m. odd m \<Longrightarrow> even (Suc m)"
+apply(tactic {* intros_tac_test @{context} 1 *})
+done
+lemma intro2:
+shows "\<And>m. even m \<Longrightarrow> odd (Suc m)"
+apply(tactic {* intros_tac_test @{context} 2 *})
 done
 ML{*fun introductions rules preds defs lthy =
 let
 fun prove_intro (i, goal) =
 Goal.prove lthy [] [] goal
-(fn {context, ...} => introductions_tac defs rules preds i context)
+(fn {context, ...} => intros_tac defs rules preds i context)
 in
 map_index prove_intro rules
 end*}
 text {* main internal function *}

changeset 190	ca0ac2e75f6d
parent 189	069d525f8f1d
child 192	2fff636e1fa0