Diffusion Isabelle fd21b4a93043

added opaque_combs and renamed hide_lams to opaque_lifting
fd21b4a93043
Actions

Description

added opaque_combs and renamed hide_lams to opaque_lifting

Details

Provenance

desharna

Authored on

Parents

rISABELLE66bff50bc5f1: tuned --- following hints by IntelliJ;

Branches

Unknown

Tags

Unknown

Event Timeline

desharna committed rISABELLEfd21b4a93043: added opaque_combs and renamed hide_lams to opaque_lifting.Jul 8 2021, 8:42 AM

Changes (81)

Path

Size

src/

Doc/

Sledgehammer/

document/

root.tex

HOL/

Algebra/

Coset.thy

Free_Abelian_Groups.thy

Generated_Groups.thy

Group.thy

Polynomial_Divisibility.thy

Product_Groups.thy

Subrings.thy

Analysis/

Abstract_Topology.thy

Abstract_Topology_2.thy

Arcwise_Connected.thy

Bochner_Integration.thy

Brouwer_Fixpoint.thy

Cartesian_Space.thy

Change_Of_Vars.thy

Complex_Transcendental.thy

Elementary_Metric_Spaces.thy

Equivalence_Lebesgue_Henstock_Integration.thy

Equivalence_Measurable_On_Borel.thy

Extended_Real_Limits.thy

Fashoda_Theorem.thy

Function_Metric.thy

Further_Topology.thy

Henstock_Kurzweil_Integration.thy

Topology_Euclidean_Space.thy

Uniform_Limit.thy

Auth/

Message.thy

Binomial.thy

Cardinals/

Wellorder_Constructions.thy

Combinatorics/

Cycles.thy

Complex_Analysis/

Cauchy_Integral_Formula.thy

Complex_Singularities.thy

Conformal_Mappings.thy

Great_Picard.thy

Riemann_Mapping.thy

Winding_Numbers.thy

Computational_Algebra/

Polynomial.thy

Deriv.thy

Homology/

Brouwer_Degree.thy

Invariance_of_Domain.thy

IMP/

Library/

Extended_Nonnegative_Real.thy

Nominal/

Examples/

Class1.thy

Nonstandard_Analysis/

NSA.thy

Probability/

Conditional_Expectation.thy

Quotient_Examples/

Lift_Fun.thy

Real.thy

Real_Vector_Spaces.thy

SPARK/

Examples/

RIPEMD-160/

Round.thy

Series.thy

Tools/

ATP/

atp_problem_generate.ML

Metis/

metis_generate.ML

metis_tactic.ML

Sledgehammer/

sledgehammer_prover_atp.ML

Transcendental.thy

Vector_Spaces.thy

ex/

Dedekind_Real.thy

rISABELLEfd21b4a93043

View Options

src/Doc/Sledgehammer/document/root.tex

View Options

src/HOL/Algebra/Coset.thy

View Options

src/HOL/Algebra/Free_Abelian_Groups.thy

View Options

src/HOL/Algebra/Generated_Groups.thy

View Options

src/HOL/Algebra/Group.thy

View Options

src/HOL/Algebra/Polynomial_Divisibility.thy

View Options

src/HOL/Algebra/Product_Groups.thy

View Options

src/HOL/Algebra/Subrings.thy

View Options

src/HOL/Analysis/Abstract_Topology.thy

View Options

src/HOL/Analysis/Abstract_Topology_2.thy

View Options

src/HOL/Analysis/Arcwise_Connected.thy

View Options

src/HOL/Analysis/Bochner_Integration.thy

View Options

src/HOL/Analysis/Brouwer_Fixpoint.thy

View Options

src/HOL/Analysis/Cartesian_Space.thy

View Options

src/HOL/Analysis/Change_Of_Vars.thy

View Options

src/HOL/Analysis/Complex_Transcendental.thy

View Options

src/HOL/Analysis/Connected.thy

View Options

src/HOL/Analysis/Cross3.thy

View Options

src/HOL/Analysis/Derivative.thy

View Options

src/HOL/Analysis/Determinants.thy

View Options

src/HOL/Analysis/Elementary_Metric_Spaces.thy

View Options

src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy

View Options

src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy

View Options

src/HOL/Analysis/Extended_Real_Limits.thy

View Options

src/HOL/Analysis/Fashoda_Theorem.thy

View Options

src/HOL/Analysis/Function_Metric.thy

View Options

src/HOL/Analysis/Further_Topology.thy

View Options

src/HOL/Analysis/Henstock_Kurzweil_Integration.thy

View Options

src/HOL/Analysis/Homotopy.thy

View Options

src/HOL/Analysis/Jordan_Curve.thy

View Options

src/HOL/Analysis/Line_Segment.thy

View Options

src/HOL/Analysis/Linear_Algebra.thy

View Options

src/HOL/Analysis/Path_Connected.thy

View Options

src/HOL/Analysis/Polytope.thy

View Options

src/HOL/Analysis/Retracts.thy

View Options

src/HOL/Analysis/Starlike.thy

View Options

src/HOL/Analysis/Tagged_Division.thy

View Options

src/HOL/Analysis/Topology_Euclidean_Space.thy

View Options

src/HOL/Analysis/Uniform_Limit.thy

View Options

src/HOL/Auth/Message.thy

View Options

src/HOL/Binomial.thy

View Options

src/HOL/Cardinals/Wellorder_Constructions.thy

View Options

src/HOL/Combinatorics/Cycles.thy

View Options

src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy

View Options

src/HOL/Complex_Analysis/Complex_Singularities.thy

View Options

src/HOL/Complex_Analysis/Conformal_Mappings.thy

View Options

src/HOL/Complex_Analysis/Great_Picard.thy

View Options

src/HOL/Complex_Analysis/Riemann_Mapping.thy

View Options

src/HOL/Complex_Analysis/Winding_Numbers.thy

View Options

src/HOL/Computational_Algebra/Polynomial.thy

View Options

src/HOL/Deriv.thy

View Options

src/HOL/Homology/Brouwer_Degree.thy

View Options

src/HOL/Homology/Invariance_of_Domain.thy

View Options

src/HOL/Homology/Simplices.thy

View Options

src/HOL/IMP/Abs_Int2.thy

View Options

src/HOL/IMP/Abs_Int3.thy

View Options

src/HOL/Library/Dlist.thy

View Options

src/HOL/Library/Equipollence.thy

View Options

src/HOL/Library/Extended_Nonnegative_Real.thy

View Options

src/HOL/Library/Extended_Real.thy

View Options

src/HOL/Library/Float.thy

View Options

src/HOL/Library/FuncSet.thy

View Options

src/HOL/Library/Interval.thy

View Options

src/HOL/Library/Poly_Mapping.thy

View Options

src/HOL/Library/Word.thy

View Options

src/HOL/List.thy

View Options

src/HOL/Nominal/Examples/Class1.thy

View Options

src/HOL/Nonstandard_Analysis/NSA.thy

View Options

src/HOL/Probability/Conditional_Expectation.thy

View Options

src/HOL/Quotient_Examples/Lift_Fun.thy

View Options

src/HOL/Real.thy

View Options

src/HOL/Real_Vector_Spaces.thy

View Options

src/HOL/SPARK/Examples/RIPEMD-160/Round.thy

View Options

src/HOL/Series.thy

View Options

src/HOL/Tools/ATP/atp_problem_generate.ML

View Options

src/HOL/Tools/Metis/metis_generate.ML

View Options

src/HOL/Tools/Metis/metis_tactic.ML

View Options

src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML

View Options

src/HOL/Transcendental.thy

View Options

src/HOL/Vector_Spaces.thy

View Options

src/HOL/ex/Dedekind_Real.thy

added opaque_combs and renamed hide_lams to opaque_liftingfd21b4a93043Actions

Description

Details

Event Timeline

Changes (81)

rISABELLEfd21b4a93043

src/Doc/Sledgehammer/document/root.tex

src/HOL/Algebra/Coset.thy

src/HOL/Algebra/Free_Abelian_Groups.thy

src/HOL/Algebra/Generated_Groups.thy

src/HOL/Algebra/Group.thy

src/HOL/Algebra/Polynomial_Divisibility.thy

src/HOL/Algebra/Product_Groups.thy

src/HOL/Algebra/Subrings.thy

src/HOL/Analysis/Abstract_Topology.thy

src/HOL/Analysis/Abstract_Topology_2.thy

src/HOL/Analysis/Arcwise_Connected.thy

src/HOL/Analysis/Bochner_Integration.thy

src/HOL/Analysis/Brouwer_Fixpoint.thy

src/HOL/Analysis/Cartesian_Space.thy

src/HOL/Analysis/Change_Of_Vars.thy

src/HOL/Analysis/Complex_Transcendental.thy

src/HOL/Analysis/Connected.thy

src/HOL/Analysis/Cross3.thy

src/HOL/Analysis/Derivative.thy

src/HOL/Analysis/Determinants.thy

src/HOL/Analysis/Elementary_Metric_Spaces.thy

src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy

src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy

src/HOL/Analysis/Extended_Real_Limits.thy

src/HOL/Analysis/Fashoda_Theorem.thy

src/HOL/Analysis/Function_Metric.thy

src/HOL/Analysis/Further_Topology.thy

src/HOL/Analysis/Henstock_Kurzweil_Integration.thy

src/HOL/Analysis/Homotopy.thy

src/HOL/Analysis/Jordan_Curve.thy

src/HOL/Analysis/Line_Segment.thy

src/HOL/Analysis/Linear_Algebra.thy

src/HOL/Analysis/Path_Connected.thy

src/HOL/Analysis/Polytope.thy

src/HOL/Analysis/Retracts.thy

src/HOL/Analysis/Starlike.thy

src/HOL/Analysis/Tagged_Division.thy

src/HOL/Analysis/Topology_Euclidean_Space.thy

src/HOL/Analysis/Uniform_Limit.thy

src/HOL/Auth/Message.thy

src/HOL/Binomial.thy

src/HOL/Cardinals/Wellorder_Constructions.thy

src/HOL/Combinatorics/Cycles.thy

src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy

src/HOL/Complex_Analysis/Complex_Singularities.thy

src/HOL/Complex_Analysis/Conformal_Mappings.thy

src/HOL/Complex_Analysis/Great_Picard.thy

src/HOL/Complex_Analysis/Riemann_Mapping.thy

src/HOL/Complex_Analysis/Winding_Numbers.thy

src/HOL/Computational_Algebra/Polynomial.thy

src/HOL/Deriv.thy

src/HOL/Homology/Brouwer_Degree.thy

src/HOL/Homology/Invariance_of_Domain.thy

src/HOL/Homology/Simplices.thy

src/HOL/IMP/Abs_Int2.thy

src/HOL/IMP/Abs_Int3.thy

src/HOL/Library/Dlist.thy

src/HOL/Library/Equipollence.thy

src/HOL/Library/Extended_Nonnegative_Real.thy

src/HOL/Library/Extended_Real.thy

src/HOL/Library/Float.thy

src/HOL/Library/FuncSet.thy

src/HOL/Library/Interval.thy

src/HOL/Library/Poly_Mapping.thy

src/HOL/Library/Word.thy

src/HOL/List.thy

src/HOL/Nominal/Examples/Class1.thy

src/HOL/Nonstandard_Analysis/NSA.thy

src/HOL/Probability/Conditional_Expectation.thy

src/HOL/Quotient_Examples/Lift_Fun.thy

src/HOL/Real.thy

src/HOL/Real_Vector_Spaces.thy

src/HOL/SPARK/Examples/RIPEMD-160/Round.thy

src/HOL/Series.thy

added opaque_combs and renamed hide_lams to opaque_lifting
fd21b4a93043
Actions