Diffusion afp-devel 2056abab0dd6

mproper proof command 'guess' moved to separate theory "Pure-ex.Guess"…
2056abab0dd6
Actions

Description

mproper proof command 'guess' moved to separate theory "Pure-ex.Guess", according to Isabelle/b49bd5d9041f;

Details

Provenance

makarius

Authored on

Parents

rAFP61b65f5bfdbe: ported Design-Theory from AFP 2021 to devel

Branches

Unknown

Tags

Unknown

Event Timeline

makarius committed rAFP2056abab0dd6: mproper proof command 'guess' moved to separate theory "Pure-ex.Guess"….Sep 26 2021, 8:12 PM

makarius mentioned this in Blog Post: Improper proof command 'guess' provided by separate theory "Pure-ex.Guess".Sep 27 2021, 5:00 PM

Changes (57)

Path

Size

thys/

Akra_Bazzi/

Akra_Bazzi_Library.thy

ROOT

Automatic_Refinement/

Lib/

Misc.thy

Bertrands_Postulate/

Bertrand.thy

DFS_Framework/

Examples/

Dirichlet_Series/

E_Transcendental/

Error_Function/

Euler_MacLaurin/

Euler_MacLaurin_Landau.thy

Fishburn_Impossibility/

Fishburn_Impossibility.thy

Social_Choice_Functions.thy

Functional-Automata/

Goodstein_Lambda/

Hoare_Time/

IFC_Tracking/

IMP2/

doc/

Examples.thy

LOFT/

LinuxRouter_OpenFlow_Translation.thy

ROOT

Landau_Symbols/

Landau_Real_Products.thy

Linear_Recurrences/

RatFPS.thy

Rational_FPS_Asymptotics.thy

Liouville_Numbers/

Liouville_Numbers.thy

Markov_Models/

Classifying_Markov_Chain_States.thy

Minsky_Machines/

Minsky.thy

ROOT

Myhill-Nerode/

Non_Regular_Languages.thy

Ordinary_Differential_Equations/

Numerics/

Refine_Rigorous_Numerics_Aform.thy

Pratt_Certificate/

Pratt_Certificate.thy

Prime_Number_Theorem/

Prime_Number_Theorem_Library.thy

Probabilistic_Timed_Automata/

library/

Propositional_Proof_Systems/

Compactness.thy

Consistency.thy

LSC_Resolution.thy

ND_Compl_Truthtable_Compact.thy

ND_FiniteAssms.thy

SC_Depth.thy

SC_Gentzen.thy

Randomised_Social_Choice/

Preference_Profiles.thy

SDS_Lowering.thy

SD_Efficiency.thy

Social_Decision_Schemes.thy

Stochastic_Dominance.thy

Routing/

ROOT

Routing_Table.thy

SDS_Impossibility/

SDS_Impossibility.thy

Stirling_Formula/

Gamma_Asymptotics.thy

Sturm_Sequences/

Lib/

Misc_Polynomial.thy

ROOT

Treaps/

Random_List_Permutation.thy

Twelvefold_Way/

Twelvefold_Way_Core.thy

UpDown_Scheme/

Triangular_Function.thy

Zeta_Function/

ROOT

Zeta_Function.thy

rAFP2056abab0dd6

View Options

thys/Akra_Bazzi/Akra_Bazzi_Library.thy

View Options

thys/Akra_Bazzi/ROOT

View Options

thys/Automatic_Refinement/Lib/Misc.thy

View Options

thys/Bertrands_Postulate/Bertrand.thy

View Options

thys/DFS_Framework/Examples/Tarjan.thy

View Options

thys/Dirichlet_Series/Dirichlet_Misc.thy

View Options

thys/E_Transcendental/E_Transcendental.thy

View Options

thys/Error_Function/Error_Function.thy

View Options

thys/Euler_MacLaurin/Euler_MacLaurin.thy

View Options

thys/Euler_MacLaurin/Euler_MacLaurin_Landau.thy

View Options

thys/Fishburn_Impossibility/Fishburn_Impossibility.thy

View Options

thys/Fishburn_Impossibility/Social_Choice_Functions.thy

View Options

thys/Functional-Automata/MaxPrefix.thy

View Options

thys/Goodstein_Lambda/Goodstein_Lambda.thy

View Options

thys/Hoare_Time/SepLogK_VCG.thy

View Options

thys/IFC_Tracking/IFC.thy

View Options

thys/IMP2/doc/Examples.thy

View Options

thys/LOFT/LinuxRouter_OpenFlow_Translation.thy

View Options

thys/LOFT/ROOT

View Options

thys/Landau_Symbols/Landau_Real_Products.thy

View Options

thys/Linear_Recurrences/RatFPS.thy

View Options

thys/Linear_Recurrences/Rational_FPS_Asymptotics.thy

View Options

thys/Liouville_Numbers/Liouville_Numbers.thy

View Options

thys/Markov_Models/Classifying_Markov_Chain_States.thy

View Options

thys/Minsky_Machines/Minsky.thy

View Options

thys/Minsky_Machines/ROOT

View Options

thys/Myhill-Nerode/Non_Regular_Languages.thy

View Options

thys/Ordinary_Differential_Equations/Numerics/Refine_Rigorous_Numerics_Aform.thy

View Options

thys/Pratt_Certificate/Pratt_Certificate.thy

View Options

thys/Prime_Number_Theorem/Prime_Number_Theorem_Library.thy

View Options

thys/Probabilistic_Timed_Automata/ROOT

View Options

thys/Probabilistic_Timed_Automata/library/Graphs.thy

View Options

thys/Probabilistic_Timed_Automata/library/More_List.thy

View Options

thys/Probabilistic_Timed_Automata/library/Stream_More.thy

View Options

thys/Propositional_Proof_Systems/Compactness.thy

View Options

thys/Propositional_Proof_Systems/Consistency.thy

View Options

thys/Propositional_Proof_Systems/LSC_Resolution.thy

View Options

thys/Propositional_Proof_Systems/ND_Compl_Truthtable_Compact.thy

View Options

thys/Propositional_Proof_Systems/ND_FiniteAssms.thy

View Options

thys/Propositional_Proof_Systems/SC_Depth.thy

View Options

thys/Propositional_Proof_Systems/SC_Gentzen.thy

View Options

thys/Randomised_Social_Choice/Preference_Profiles.thy

View Options

thys/Randomised_Social_Choice/SDS_Lowering.thy

View Options

thys/Randomised_Social_Choice/SD_Efficiency.thy

View Options

thys/Randomised_Social_Choice/Social_Decision_Schemes.thy

View Options

thys/Randomised_Social_Choice/Stochastic_Dominance.thy

View Options

thys/Routing/ROOT

View Options

thys/Routing/Routing_Table.thy

View Options

thys/SDS_Impossibility/SDS_Impossibility.thy

View Options

thys/Stirling_Formula/Gamma_Asymptotics.thy

View Options

thys/Sturm_Sequences/Lib/Misc_Polynomial.thy

View Options

thys/Sturm_Sequences/ROOT

View Options

thys/Treaps/Random_List_Permutation.thy

View Options

thys/Twelvefold_Way/Twelvefold_Way_Core.thy

View Options

thys/UpDown_Scheme/Triangular_Function.thy

View Options

thys/Zeta_Function/ROOT

View Options

thys/Zeta_Function/Zeta_Function.thy

mproper proof command 'guess' moved to separate theory "Pure-ex.Guess"…2056abab0dd6Actions

Description

Details

Event Timeline

Changes (57)

rAFP2056abab0dd6

thys/Akra_Bazzi/Akra_Bazzi_Library.thy

thys/Akra_Bazzi/ROOT

thys/Automatic_Refinement/Lib/Misc.thy

thys/Bertrands_Postulate/Bertrand.thy

thys/DFS_Framework/Examples/Tarjan.thy

thys/Dirichlet_Series/Dirichlet_Misc.thy

thys/E_Transcendental/E_Transcendental.thy

thys/Error_Function/Error_Function.thy

thys/Euler_MacLaurin/Euler_MacLaurin.thy

thys/Euler_MacLaurin/Euler_MacLaurin_Landau.thy

thys/Fishburn_Impossibility/Fishburn_Impossibility.thy

thys/Fishburn_Impossibility/Social_Choice_Functions.thy

thys/Functional-Automata/MaxPrefix.thy

thys/Goodstein_Lambda/Goodstein_Lambda.thy

thys/Hoare_Time/SepLogK_VCG.thy

thys/IFC_Tracking/IFC.thy

thys/IMP2/doc/Examples.thy

thys/LOFT/LinuxRouter_OpenFlow_Translation.thy

thys/LOFT/ROOT

thys/Landau_Symbols/Landau_Real_Products.thy

thys/Linear_Recurrences/RatFPS.thy

thys/Linear_Recurrences/Rational_FPS_Asymptotics.thy

thys/Liouville_Numbers/Liouville_Numbers.thy

thys/Markov_Models/Classifying_Markov_Chain_States.thy

thys/Minsky_Machines/Minsky.thy

thys/Minsky_Machines/ROOT

thys/Myhill-Nerode/Non_Regular_Languages.thy

thys/Ordinary_Differential_Equations/Numerics/Refine_Rigorous_Numerics_Aform.thy

thys/Pratt_Certificate/Pratt_Certificate.thy

thys/Prime_Number_Theorem/Prime_Number_Theorem_Library.thy

thys/Probabilistic_Timed_Automata/ROOT

thys/Probabilistic_Timed_Automata/library/Graphs.thy

thys/Probabilistic_Timed_Automata/library/More_List.thy

thys/Probabilistic_Timed_Automata/library/Stream_More.thy

thys/Propositional_Proof_Systems/Compactness.thy

thys/Propositional_Proof_Systems/Consistency.thy

thys/Propositional_Proof_Systems/LSC_Resolution.thy

thys/Propositional_Proof_Systems/ND_Compl_Truthtable_Compact.thy

thys/Propositional_Proof_Systems/ND_FiniteAssms.thy

thys/Propositional_Proof_Systems/SC_Depth.thy

thys/Propositional_Proof_Systems/SC_Gentzen.thy

thys/Randomised_Social_Choice/Preference_Profiles.thy

thys/Randomised_Social_Choice/SDS_Lowering.thy

thys/Randomised_Social_Choice/SD_Efficiency.thy

thys/Randomised_Social_Choice/Social_Decision_Schemes.thy

thys/Randomised_Social_Choice/Stochastic_Dominance.thy

thys/Routing/ROOT

thys/Routing/Routing_Table.thy

thys/SDS_Impossibility/SDS_Impossibility.thy

thys/Stirling_Formula/Gamma_Asymptotics.thy

thys/Sturm_Sequences/Lib/Misc_Polynomial.thy

thys/Sturm_Sequences/ROOT

thys/Treaps/Random_List_Permutation.thy

thys/Twelvefold_Way/Twelvefold_Way_Core.thy

thys/UpDown_Scheme/Triangular_Function.thy

thys/Zeta_Function/ROOT

thys/Zeta_Function/Zeta_Function.thy

mproper proof command 'guess' moved to separate theory "Pure-ex.Guess"…
2056abab0dd6
Actions