Changes

Summary

fix import in List_Factoring
checking in some work on analysis of BIT MTF TS and OPT2
merge
minor changes on BIT, Competitive_Analysis mtf2effects and work on List_Factoring
ability to select different factorization oracles

Changeset 6272:a28d2d2ded2d by max haslbeck _haslbema@in.tum.de_: fix import in List_Factoring
The file was modified	`thys/Amortized_Complexity/List_Factoring.thy` (diff)
Changeset 6271:7467b21195a8 by max haslbeck _haslbema@in.tum.de_: checking in some work on analysis of BIT MTF TS and OPT2
The file was added	`thys/Amortized_Complexity/BIT_2comp_on2.thy`
The file was added	`thys/Amortized_Complexity/BIT_pairwise.thy`
The file was added	`thys/Amortized_Complexity/MTF_2comp_on2.thy`
The file was added	`thys/Amortized_Complexity/MTF_pairwise.thy`
The file was added	`thys/Amortized_Complexity/OPT2.thy`
The file was added	`thys/Amortized_Complexity/Partial_Cost_Model.thy`
The file was added	`thys/Amortized_Complexity/Phase_Partitioning.thy`
The file was added	`thys/Amortized_Complexity/RExp_Var.thy`
The file was added	`thys/Amortized_Complexity/TS.thy`
Changeset 6270:b841a1a203fc by max haslbeck _haslbema@in.tum.de_: merge
Changeset 6269:1479f23e980f by max haslbeck _haslbema@in.tum.de_: minor changes on BIT, Competitive_Analysis mtf2effects and work on List_Factoring
The file was modified	`thys/Amortized_Complexity/BIT.thy` (diff)
The file was modified	`thys/Amortized_Complexity/Competitive_Analysis.thy` (diff)
The file was modified	`thys/Amortized_Complexity/List_Factoring.thy` (diff)
The file was modified	`thys/Amortized_Complexity/mtf2_effects.thy` (diff)
Changeset 6268:4023c425b491 by rene thiemann _rene.thiemann@uibk.ac.at_: ability to select different factorization oracles
The file was added	`thys/Polynomial_Factorization/External_Factorization.thy`
The file was added	`thys/Polynomial_Factorization/Hybrid_Factorization.thy`
The file was added	`thys/Polynomial_Factorization/Select_Berlekamp_Hensel_Factorization.thy`
The file was added	`thys/Polynomial_Factorization/Select_External_Factorization.thy`
The file was added	`thys/Polynomial_Factorization/Select_Hybrid_Factorization.thy`
The file was modified	`thys/Algebraic_Numbers/Algebraic_Number_Tests.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Real_Algebraic_Numbers.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Berlekamp_Hensel_Factorization.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Factorization_Oracle.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/ROOT` (diff)
The file was modified	`thys/Polynomial_Factorization/Rational_Factorization.thy` (diff)