Changes

Summary

Replaced theory "Buchberger_Algorithm" by "Algorithm_Schema" and "Buchberger"
Added lemmas and slightly re-structured theories
Based ideals and linear hulls of polynomials on generic type-class modules

Changeset 8954:f70c302d6bc4 by alexander maletzky _alexander.maletzky@risc.jku.at_: Replaced theory "Buchberger_Algorithm" by "Algorithm_Schema" and "Buchberger"
The file was added	`thys/Groebner_Bases/Algorithm_Schema.thy`
The file was added	`thys/Groebner_Bases/Algorithm_Schema_Impl.thy`
The file was added	`thys/Groebner_Bases/Buchberger.thy`
The file was added	`thys/Groebner_Bases/Buchberger_Examples.thy`
The file was modified	`thys/Groebner_Bases/General.thy` (diff)
The file was modified	`thys/Groebner_Bases/Groebner_Bases.thy` (diff)
The file was modified	`thys/Groebner_Bases/ROOT` (diff)
The file was modified	`thys/Polynomials/MPoly_Type_Class.thy` (diff)
The file was removed	`thys/Groebner_Bases/Buchberger_Algorithm.thy`
The file was removed	`thys/Groebner_Bases/Computations.thy`
Changeset 8953:dc22745d77b5 by alexander maletzky _alexander.maletzky@risc.jku.at_: Added lemmas and slightly re-structured theories
The file was modified	`thys/Groebner_Bases/General.thy` (diff)
The file was modified	`thys/Groebner_Bases/Groebner_Bases.thy` (diff)
The file was modified	`thys/Polynomials/MPoly_Type_Class.thy` (diff)
The file was modified	`thys/Polynomials/MPoly_Type_Class_FMap.thy` (diff)
The file was modified	`thys/Polynomials/Power_Products.thy` (diff)
The file was modified	`thys/Polynomials/Utils.thy` (diff)
Changeset 8952:0f557298e73e by alexander maletzky _alexander.maletzky@risc.jku.at_: Based ideals and linear hulls of polynomials on generic type-class modules
The file was added	`thys/Polynomials/Module_Type_Class.thy`
The file was modified	`thys/Groebner_Bases/Buchberger_Algorithm.thy` (diff)
The file was modified	`thys/Groebner_Bases/Groebner_Bases.thy` (diff)
The file was modified	`thys/Groebner_Bases/Reduction.thy` (diff)
The file was modified	`thys/Polynomials/MPoly_Type_Class.thy` (diff)