wenzelm@9487: (*  Title:      FOL/FOL.thy
wenzelm@9487:     Author:     Lawrence C Paulson and Markus Wenzel
wenzelm@11678: *)
wenzelm@9487: 
wenzelm@11678: header {* Classical first-order logic *}
wenzelm@4093: 
wenzelm@18456: theory FOL
paulson@15481: imports IFOL
wenzelm@46950: keywords "print_claset" "print_induct_rules" :: diag
wenzelm@18456: begin
wenzelm@9487: 
wenzelm@48891: ML_file "~~/src/Provers/classical.ML"
wenzelm@48891: ML_file "~~/src/Provers/blast.ML"
wenzelm@48891: ML_file "~~/src/Provers/clasimp.ML"
wenzelm@48891: ML_file "~~/src/Tools/induct.ML"
wenzelm@48891: ML_file "~~/src/Tools/case_product.ML"
wenzelm@48891: 
wenzelm@9487: 
wenzelm@9487: subsection {* The classical axiom *}
wenzelm@4093: 
wenzelm@41779: axiomatization where
wenzelm@7355:   classical: "(~P ==> P) ==> P"
wenzelm@4093: 
wenzelm@9487: 
wenzelm@11678: subsection {* Lemmas and proof tools *}
wenzelm@9487: 
wenzelm@21539: lemma ccontr: "(\<not> P \<Longrightarrow> False) \<Longrightarrow> P"
wenzelm@21539:   by (erule FalseE [THEN classical])
wenzelm@21539: 
wenzelm@21539: (*** Classical introduction rules for | and EX ***)
wenzelm@21539: 
wenzelm@21539: lemma disjCI: "(~Q ==> P) ==> P|Q"
wenzelm@21539:   apply (rule classical)
wenzelm@21539:   apply (assumption | erule meta_mp | rule disjI1 notI)+
wenzelm@21539:   apply (erule notE disjI2)+
wenzelm@21539:   done
wenzelm@21539: 
wenzelm@21539: (*introduction rule involving only EX*)
wenzelm@21539: lemma ex_classical:
wenzelm@21539:   assumes r: "~(EX x. P(x)) ==> P(a)"
wenzelm@21539:   shows "EX x. P(x)"
wenzelm@21539:   apply (rule classical)
wenzelm@21539:   apply (rule exI, erule r)
wenzelm@21539:   done
wenzelm@21539: 
wenzelm@21539: (*version of above, simplifying ~EX to ALL~ *)
wenzelm@21539: lemma exCI:
wenzelm@21539:   assumes r: "ALL x. ~P(x) ==> P(a)"
wenzelm@21539:   shows "EX x. P(x)"
wenzelm@21539:   apply (rule ex_classical)
wenzelm@21539:   apply (rule notI [THEN allI, THEN r])
wenzelm@21539:   apply (erule notE)
wenzelm@21539:   apply (erule exI)
wenzelm@21539:   done
wenzelm@21539: 
wenzelm@21539: lemma excluded_middle: "~P | P"
wenzelm@21539:   apply (rule disjCI)
wenzelm@21539:   apply assumption
wenzelm@21539:   done
wenzelm@21539: 
wenzelm@27115: lemma case_split [case_names True False]:
wenzelm@21539:   assumes r1: "P ==> Q"
wenzelm@21539:     and r2: "~P ==> Q"
wenzelm@21539:   shows Q
wenzelm@21539:   apply (rule excluded_middle [THEN disjE])
wenzelm@21539:   apply (erule r2)
wenzelm@21539:   apply (erule r1)
wenzelm@21539:   done
wenzelm@21539: 
wenzelm@21539: ML {*
wenzelm@27239:   fun case_tac ctxt a = res_inst_tac ctxt [(("P", 0), a)] @{thm case_split}
wenzelm@21539: *}
wenzelm@21539: 
wenzelm@30549: method_setup case_tac = {*
wenzelm@55111:   Args.goal_spec -- Scan.lift Args.name_inner_syntax >>
wenzelm@42814:     (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s))
wenzelm@30549: *} "case_tac emulation (dynamic instantiation!)"
wenzelm@27211: 
wenzelm@21539: 
wenzelm@21539: (*** Special elimination rules *)
wenzelm@21539: 
wenzelm@21539: 
wenzelm@21539: (*Classical implies (-->) elimination. *)
wenzelm@21539: lemma impCE:
wenzelm@21539:   assumes major: "P-->Q"
wenzelm@21539:     and r1: "~P ==> R"
wenzelm@21539:     and r2: "Q ==> R"
wenzelm@21539:   shows R
wenzelm@21539:   apply (rule excluded_middle [THEN disjE])
wenzelm@21539:    apply (erule r1)
wenzelm@21539:   apply (rule r2)
wenzelm@21539:   apply (erule major [THEN mp])
wenzelm@21539:   done
wenzelm@21539: 
wenzelm@21539: (*This version of --> elimination works on Q before P.  It works best for
wenzelm@21539:   those cases in which P holds "almost everywhere".  Can't install as
wenzelm@21539:   default: would break old proofs.*)
wenzelm@21539: lemma impCE':
wenzelm@21539:   assumes major: "P-->Q"
wenzelm@21539:     and r1: "Q ==> R"
wenzelm@21539:     and r2: "~P ==> R"
wenzelm@21539:   shows R
wenzelm@21539:   apply (rule excluded_middle [THEN disjE])
wenzelm@21539:    apply (erule r2)
wenzelm@21539:   apply (rule r1)
wenzelm@21539:   apply (erule major [THEN mp])
wenzelm@21539:   done
wenzelm@21539: 
wenzelm@21539: (*Double negation law*)
wenzelm@21539: lemma notnotD: "~~P ==> P"
wenzelm@21539:   apply (rule classical)
wenzelm@21539:   apply (erule notE)
wenzelm@21539:   apply assumption
wenzelm@21539:   done
wenzelm@21539: 
wenzelm@21539: lemma contrapos2:  "[| Q; ~ P ==> ~ Q |] ==> P"
wenzelm@21539:   apply (rule classical)
wenzelm@21539:   apply (drule (1) meta_mp)
wenzelm@21539:   apply (erule (1) notE)
wenzelm@21539:   done
wenzelm@21539: 
wenzelm@21539: (*** Tactics for implication and contradiction ***)
wenzelm@21539: 
wenzelm@42453: (*Classical <-> elimination.  Proof substitutes P=Q in
wenzelm@21539:     ~P ==> ~Q    and    P ==> Q  *)
wenzelm@21539: lemma iffCE:
wenzelm@21539:   assumes major: "P<->Q"
wenzelm@21539:     and r1: "[| P; Q |] ==> R"
wenzelm@21539:     and r2: "[| ~P; ~Q |] ==> R"
wenzelm@21539:   shows R
wenzelm@21539:   apply (rule major [unfolded iff_def, THEN conjE])
wenzelm@21539:   apply (elim impCE)
wenzelm@21539:      apply (erule (1) r2)
wenzelm@21539:     apply (erule (1) notE)+
wenzelm@21539:   apply (erule (1) r1)
wenzelm@21539:   done
wenzelm@21539: 
wenzelm@21539: 
wenzelm@21539: (*Better for fast_tac: needs no quantifier duplication!*)
wenzelm@21539: lemma alt_ex1E:
wenzelm@21539:   assumes major: "EX! x. P(x)"
wenzelm@21539:     and r: "!!x. [| P(x);  ALL y y'. P(y) & P(y') --> y=y' |] ==> R"
wenzelm@21539:   shows R
wenzelm@21539:   using major
wenzelm@21539: proof (rule ex1E)
wenzelm@21539:   fix x
wenzelm@21539:   assume * : "\<forall>y. P(y) \<longrightarrow> y = x"
wenzelm@21539:   assume "P(x)"
wenzelm@21539:   then show R
wenzelm@21539:   proof (rule r)
wenzelm@21539:     { fix y y'
wenzelm@21539:       assume "P(y)" and "P(y')"
wenzelm@51798:       with * have "x = y" and "x = y'" by - (tactic "IntPr.fast_tac @{context} 1")+
wenzelm@21539:       then have "y = y'" by (rule subst)
wenzelm@21539:     } note r' = this
wenzelm@21539:     show "\<forall>y y'. P(y) \<and> P(y') \<longrightarrow> y = y'" by (intro strip, elim conjE) (rule r')
wenzelm@21539:   qed
wenzelm@21539: qed
wenzelm@9525: 
wenzelm@26411: lemma imp_elim: "P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R"
wenzelm@26411:   by (rule classical) iprover
wenzelm@26411: 
wenzelm@26411: lemma swap: "~ P ==> (~ R ==> P) ==> R"
wenzelm@26411:   by (rule classical) iprover
wenzelm@26411: 
wenzelm@27849: 
wenzelm@27849: section {* Classical Reasoner *}
wenzelm@27849: 
wenzelm@42793: ML {*
wenzelm@42799: structure Cla = Classical
wenzelm@42793: (
wenzelm@42793:   val imp_elim = @{thm imp_elim}
wenzelm@42793:   val not_elim = @{thm notE}
wenzelm@42793:   val swap = @{thm swap}
wenzelm@42793:   val classical = @{thm classical}
wenzelm@42793:   val sizef = size_of_thm
wenzelm@42793:   val hyp_subst_tacs = [hyp_subst_tac]
wenzelm@42793: );
wenzelm@42793: 
wenzelm@42793: structure Basic_Classical: BASIC_CLASSICAL = Cla;
wenzelm@42793: open Basic_Classical;
wenzelm@42793: *}
wenzelm@42793: 
wenzelm@10383: setup Cla.setup
wenzelm@42793: 
wenzelm@42793: (*Propositional rules*)
wenzelm@42793: lemmas [intro!] = refl TrueI conjI disjCI impI notI iffI
wenzelm@42793:   and [elim!] = conjE disjE impCE FalseE iffCE
wenzelm@51687: ML {* val prop_cs = claset_of @{context} *}
wenzelm@42793: 
wenzelm@42793: (*Quantifier rules*)
wenzelm@42793: lemmas [intro!] = allI ex_ex1I
wenzelm@42793:   and [intro] = exI
wenzelm@42793:   and [elim!] = exE alt_ex1E
wenzelm@42793:   and [elim] = allE
wenzelm@51687: ML {* val FOL_cs = claset_of @{context} *}
wenzelm@10383: 
wenzelm@32176: ML {*
wenzelm@32176:   structure Blast = Blast
wenzelm@32176:   (
wenzelm@42477:     structure Classical = Cla
wenzelm@42802:     val Trueprop_const = dest_Const @{const Trueprop}
wenzelm@41310:     val equality_name = @{const_name eq}
wenzelm@32176:     val not_name = @{const_name Not}
wenzelm@32960:     val notE = @{thm notE}
wenzelm@32960:     val ccontr = @{thm ccontr}
wenzelm@32176:     val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
wenzelm@32176:   );
wenzelm@32176:   val blast_tac = Blast.blast_tac;
wenzelm@32176: *}
wenzelm@32176: 
wenzelm@9487: setup Blast.setup
paulson@13550: 
paulson@13550: 
paulson@13550: lemma ex1_functional: "[| EX! z. P(a,z);  P(a,b);  P(a,c) |] ==> b = c"
wenzelm@21539:   by blast
wenzelm@20223: 
wenzelm@20223: (* Elimination of True from asumptions: *)
wenzelm@20223: lemma True_implies_equals: "(True ==> PROP P) == PROP P"
wenzelm@20223: proof
wenzelm@20223:   assume "True \<Longrightarrow> PROP P"
wenzelm@20223:   from this and TrueI show "PROP P" .
wenzelm@20223: next
wenzelm@20223:   assume "PROP P"
wenzelm@20223:   then show "PROP P" .
wenzelm@20223: qed
wenzelm@9487: 
wenzelm@21539: lemma uncurry: "P --> Q --> R ==> P & Q --> R"
wenzelm@21539:   by blast
wenzelm@21539: 
wenzelm@21539: lemma iff_allI: "(!!x. P(x) <-> Q(x)) ==> (ALL x. P(x)) <-> (ALL x. Q(x))"
wenzelm@21539:   by blast
wenzelm@21539: 
wenzelm@21539: lemma iff_exI: "(!!x. P(x) <-> Q(x)) ==> (EX x. P(x)) <-> (EX x. Q(x))"
wenzelm@21539:   by blast
wenzelm@21539: 
wenzelm@21539: lemma all_comm: "(ALL x y. P(x,y)) <-> (ALL y x. P(x,y))" by blast
wenzelm@21539: 
wenzelm@21539: lemma ex_comm: "(EX x y. P(x,y)) <-> (EX y x. P(x,y))" by blast
wenzelm@21539: 
wenzelm@26286: 
wenzelm@26286: 
wenzelm@26286: (*** Classical simplification rules ***)
wenzelm@26286: 
wenzelm@26286: (*Avoids duplication of subgoals after expand_if, when the true and false
wenzelm@26286:   cases boil down to the same thing.*)
wenzelm@26286: lemma cases_simp: "(P --> Q) & (~P --> Q) <-> Q" by blast
wenzelm@26286: 
wenzelm@26286: 
wenzelm@26286: (*** Miniscoping: pushing quantifiers in
wenzelm@26286:      We do NOT distribute of ALL over &, or dually that of EX over |
wenzelm@26286:      Baaz and Leitsch, On Skolemization and Proof Complexity (1994)
wenzelm@26286:      show that this step can increase proof length!
wenzelm@26286: ***)
wenzelm@26286: 
wenzelm@26286: (*existential miniscoping*)
wenzelm@26286: lemma int_ex_simps:
wenzelm@26286:   "!!P Q. (EX x. P(x) & Q) <-> (EX x. P(x)) & Q"
wenzelm@26286:   "!!P Q. (EX x. P & Q(x)) <-> P & (EX x. Q(x))"
wenzelm@26286:   "!!P Q. (EX x. P(x) | Q) <-> (EX x. P(x)) | Q"
wenzelm@26286:   "!!P Q. (EX x. P | Q(x)) <-> P | (EX x. Q(x))"
wenzelm@26286:   by iprover+
wenzelm@26286: 
wenzelm@26286: (*classical rules*)
wenzelm@26286: lemma cla_ex_simps:
wenzelm@26286:   "!!P Q. (EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q"
wenzelm@26286:   "!!P Q. (EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"
wenzelm@26286:   by blast+
wenzelm@26286: 
wenzelm@26286: lemmas ex_simps = int_ex_simps cla_ex_simps
wenzelm@26286: 
wenzelm@26286: (*universal miniscoping*)
wenzelm@26286: lemma int_all_simps:
wenzelm@26286:   "!!P Q. (ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q"
wenzelm@26286:   "!!P Q. (ALL x. P & Q(x)) <-> P & (ALL x. Q(x))"
wenzelm@26286:   "!!P Q. (ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q"
wenzelm@26286:   "!!P Q. (ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))"
wenzelm@26286:   by iprover+
wenzelm@26286: 
wenzelm@26286: (*classical rules*)
wenzelm@26286: lemma cla_all_simps:
wenzelm@26286:   "!!P Q. (ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q"
wenzelm@26286:   "!!P Q. (ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"
wenzelm@26286:   by blast+
wenzelm@26286: 
wenzelm@26286: lemmas all_simps = int_all_simps cla_all_simps
wenzelm@26286: 
wenzelm@26286: 
wenzelm@26286: (*** Named rewrite rules proved for IFOL ***)
wenzelm@26286: 
wenzelm@26286: lemma imp_disj1: "(P-->Q) | R <-> (P-->Q | R)" by blast
wenzelm@26286: lemma imp_disj2: "Q | (P-->R) <-> (P-->Q | R)" by blast
wenzelm@26286: 
wenzelm@26286: lemma de_Morgan_conj: "(~(P & Q)) <-> (~P | ~Q)" by blast
wenzelm@26286: 
wenzelm@26286: lemma not_imp: "~(P --> Q) <-> (P & ~Q)" by blast
wenzelm@26286: lemma not_iff: "~(P <-> Q) <-> (P <-> ~Q)" by blast
wenzelm@26286: 
wenzelm@26286: lemma not_all: "(~ (ALL x. P(x))) <-> (EX x.~P(x))" by blast
wenzelm@26286: lemma imp_all: "((ALL x. P(x)) --> Q) <-> (EX x. P(x) --> Q)" by blast
wenzelm@26286: 
wenzelm@26286: 
wenzelm@26286: lemmas meta_simps =
wenzelm@26286:   triv_forall_equality (* prunes params *)
wenzelm@26286:   True_implies_equals  (* prune asms `True' *)
wenzelm@26286: 
wenzelm@26286: lemmas IFOL_simps =
wenzelm@26286:   refl [THEN P_iff_T] conj_simps disj_simps not_simps
wenzelm@26286:   imp_simps iff_simps quant_simps
wenzelm@26286: 
wenzelm@26286: lemma notFalseI: "~False" by iprover
wenzelm@26286: 
wenzelm@26286: lemma cla_simps_misc:
wenzelm@26286:   "~(P&Q) <-> ~P | ~Q"
wenzelm@26286:   "P | ~P"
wenzelm@26286:   "~P | P"
wenzelm@26286:   "~ ~ P <-> P"
wenzelm@26286:   "(~P --> P) <-> P"
wenzelm@26286:   "(~P <-> ~Q) <-> (P<->Q)" by blast+
wenzelm@26286: 
wenzelm@26286: lemmas cla_simps =
wenzelm@26286:   de_Morgan_conj de_Morgan_disj imp_disj1 imp_disj2
wenzelm@26286:   not_imp not_all not_ex cases_simp cla_simps_misc
wenzelm@26286: 
wenzelm@26286: 
wenzelm@48891: ML_file "simpdata.ML"
wenzelm@42455: 
wenzelm@42459: simproc_setup defined_Ex ("EX x. P(x)") = {* fn _ => Quantifier1.rearrange_ex *}
wenzelm@42459: simproc_setup defined_All ("ALL x. P(x)") = {* fn _ => Quantifier1.rearrange_all *}
wenzelm@42455: 
wenzelm@42453: ML {*
wenzelm@42453: (*intuitionistic simprules only*)
wenzelm@42453: val IFOL_ss =
wenzelm@51717:   put_simpset FOL_basic_ss @{context}
wenzelm@45654:   addsimps @{thms meta_simps IFOL_simps int_ex_simps int_all_simps}
wenzelm@42455:   addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}]
wenzelm@51717:   |> Simplifier.add_cong @{thm imp_cong}
wenzelm@51717:   |> simpset_of;
wenzelm@42453: 
wenzelm@42453: (*classical simprules too*)
wenzelm@51717: val FOL_ss =
wenzelm@51717:   put_simpset IFOL_ss @{context}
wenzelm@51717:   addsimps @{thms cla_simps cla_ex_simps cla_all_simps}
wenzelm@51717:   |> simpset_of;
wenzelm@42453: *}
wenzelm@42453: 
wenzelm@51717: setup {* map_theory_simpset (put_simpset FOL_ss) *}
wenzelm@42455: 
wenzelm@9487: setup "Simplifier.method_setup Splitter.split_modifiers"
wenzelm@9487: setup Splitter.setup
wenzelm@26496: setup clasimp_setup
wenzelm@52241: 
wenzelm@52241: ML_file "~~/src/Tools/eqsubst.ML"
wenzelm@18591: setup EqSubst.setup
paulson@15481: 
paulson@15481: 
paulson@14085: subsection {* Other simple lemmas *}
paulson@14085: 
paulson@14085: lemma [simp]: "((P-->R) <-> (Q-->R)) <-> ((P<->Q) | R)"
paulson@14085: by blast
paulson@14085: 
paulson@14085: lemma [simp]: "((P-->Q) <-> (P-->R)) <-> (P --> (Q<->R))"
paulson@14085: by blast
paulson@14085: 
paulson@14085: lemma not_disj_iff_imp: "~P | Q <-> (P-->Q)"
paulson@14085: by blast
paulson@14085: 
paulson@14085: (** Monotonicity of implications **)
paulson@14085: 
paulson@14085: lemma conj_mono: "[| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)"
paulson@14085: by fast (*or (IntPr.fast_tac 1)*)
paulson@14085: 
paulson@14085: lemma disj_mono: "[| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)"
paulson@14085: by fast (*or (IntPr.fast_tac 1)*)
paulson@14085: 
paulson@14085: lemma imp_mono: "[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)"
paulson@14085: by fast (*or (IntPr.fast_tac 1)*)
paulson@14085: 
paulson@14085: lemma imp_refl: "P-->P"
paulson@14085: by (rule impI, assumption)
paulson@14085: 
paulson@14085: (*The quantifier monotonicity rules are also intuitionistically valid*)
paulson@14085: lemma ex_mono: "(!!x. P(x) --> Q(x)) ==> (EX x. P(x)) --> (EX x. Q(x))"
paulson@14085: by blast
paulson@14085: 
paulson@14085: lemma all_mono: "(!!x. P(x) --> Q(x)) ==> (ALL x. P(x)) --> (ALL x. Q(x))"
paulson@14085: by blast
paulson@14085: 
wenzelm@11678: 
wenzelm@11678: subsection {* Proof by cases and induction *}
wenzelm@11678: 
wenzelm@11678: text {* Proper handling of non-atomic rule statements. *}
wenzelm@11678: 
wenzelm@36866: definition "induct_forall(P) == \<forall>x. P(x)"
wenzelm@36866: definition "induct_implies(A, B) == A \<longrightarrow> B"
wenzelm@36866: definition "induct_equal(x, y) == x = y"
wenzelm@36866: definition "induct_conj(A, B) == A \<and> B"
wenzelm@11678: 
wenzelm@11678: lemma induct_forall_eq: "(!!x. P(x)) == Trueprop(induct_forall(\<lambda>x. P(x)))"
wenzelm@18816:   unfolding atomize_all induct_forall_def .
wenzelm@11678: 
wenzelm@11678: lemma induct_implies_eq: "(A ==> B) == Trueprop(induct_implies(A, B))"
wenzelm@18816:   unfolding atomize_imp induct_implies_def .
wenzelm@11678: 
wenzelm@11678: lemma induct_equal_eq: "(x == y) == Trueprop(induct_equal(x, y))"
wenzelm@18816:   unfolding atomize_eq induct_equal_def .
wenzelm@11678: 
wenzelm@28856: lemma induct_conj_eq: "(A &&& B) == Trueprop(induct_conj(A, B))"
wenzelm@18816:   unfolding atomize_conj induct_conj_def .
wenzelm@11988: 
wenzelm@18456: lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
wenzelm@45594: lemmas induct_rulify [symmetric] = induct_atomize
wenzelm@18456: lemmas induct_rulify_fallback =
wenzelm@18456:   induct_forall_def induct_implies_def induct_equal_def induct_conj_def
wenzelm@11678: 
wenzelm@36176: hide_const induct_forall induct_implies induct_equal induct_conj
wenzelm@11678: 
wenzelm@11678: 
wenzelm@11678: text {* Method setup. *}
wenzelm@11678: 
wenzelm@11678: ML {*
wenzelm@32171:   structure Induct = Induct
wenzelm@24830:   (
wenzelm@22139:     val cases_default = @{thm case_split}
wenzelm@22139:     val atomize = @{thms induct_atomize}
wenzelm@22139:     val rulify = @{thms induct_rulify}
wenzelm@22139:     val rulify_fallback = @{thms induct_rulify_fallback}
berghofe@34989:     val equal_def = @{thm induct_equal_def}
berghofe@34914:     fun dest_def _ = NONE
berghofe@34914:     fun trivial_tac _ = no_tac
wenzelm@24830:   );
wenzelm@11678: *}
wenzelm@11678: 
wenzelm@24830: setup Induct.setup
wenzelm@24830: declare case_split [cases type: o]
wenzelm@11678: 
noschinl@41827: setup Case_Product.setup
noschinl@41827: 
wenzelm@41310: 
wenzelm@41310: hide_const (open) eq
wenzelm@41310: 
wenzelm@4854: end