Changes

Summary

merge from AFP-2017
removed disturbing 'and' in author list of metadata
website for Ordered_Resolution_Prover
new entry: Ordered_Resolution_Prover

Changeset 8797:45181c49c624 by rene thiemann _rene.thiemann@uibk.ac.at_: merge from AFP-2017
Changeset 8796:41f8c8c84179 by rene thiemann _rene.thiemann@uibk.ac.at_: removed disturbing 'and' in author list of metadata
The file was modified	`metadata/metadata` (diff)
The file was modified	`web/entries/Lambda_Free_KBOs.html` (diff)
The file was modified	`web/entries/Lambda_Free_RPOs.html` (diff)
The file was modified	`web/entries/Ordered_Resolution_Prover.html` (diff)
The file was modified	`web/index.html` (diff)
The file was modified	`web/rss.xml` (diff)
The file was modified	`web/statistics.html` (diff)
Changeset 8795:0952074856d5 by rene thiemann _rene.thiemann@uibk.ac.at_: website for Ordered_Resolution_Prover
The file was added	`web/entries/Ordered_Resolution_Prover.html`
The file was modified	`metadata/metadata` (diff)
The file was modified	`web/entries/Abstract_Completeness.html` (diff)
The file was modified	`web/entries/Abstract_Soundness.html` (diff)
The file was modified	`web/entries/Coinductive.html` (diff)
The file was modified	`web/entries/FOL_Harrison.html` (diff)
The file was modified	`web/entries/Huffman.html` (diff)
The file was modified	`web/entries/Lambda_Free_KBOs.html` (diff)
The file was modified	`web/entries/Lambda_Free_RPOs.html` (diff)
The file was modified	`web/entries/Nested_Multisets_Ordinals.html` (diff)
The file was modified	`web/entries/Paraconsistency.html` (diff)
The file was modified	`web/entries/Resolution_FOL.html` (diff)
The file was modified	`web/entries/Sort_Encodings.html` (diff)
The file was modified	`web/index.html` (diff)
The file was modified	`web/rss.xml` (diff)
The file was modified	`web/statistics.html` (diff)
The file was modified	`web/topics.html` (diff)
Changeset 8794:f95facd18cb4 by rene thiemann _rene.thiemann@uibk.ac.at_: new entry: Ordered_Resolution_Prover
The file was added	`thys/Ordered_Resolution_Prover/Abstract_Substitution.thy`
The file was added	`thys/Ordered_Resolution_Prover/Clausal_Logic.thy`
The file was added	`thys/Ordered_Resolution_Prover/FO_Ordered_Resolution.thy`
The file was added	`thys/Ordered_Resolution_Prover/FO_Ordered_Resolution_Prover.thy`
The file was added	`thys/Ordered_Resolution_Prover/Ground_Resolution_Model.thy`
The file was added	`thys/Ordered_Resolution_Prover/Herbrand_Interpretation.thy`
The file was added	`thys/Ordered_Resolution_Prover/Inference_System.thy`
The file was added	`thys/Ordered_Resolution_Prover/Lazy_List_Chain.thy`
The file was added	`thys/Ordered_Resolution_Prover/Lazy_List_Liminf.thy`
The file was added	`thys/Ordered_Resolution_Prover/Map2.thy`
The file was added	`thys/Ordered_Resolution_Prover/Ordered_Ground_Resolution.thy`
The file was added	`thys/Ordered_Resolution_Prover/Proving_Process.thy`
The file was added	`thys/Ordered_Resolution_Prover/ROOT`
The file was added	`thys/Ordered_Resolution_Prover/Standard_Redundancy.thy`
The file was added	`thys/Ordered_Resolution_Prover/Unordered_Ground_Resolution.thy`
The file was added	`thys/Ordered_Resolution_Prover/document/root.tex`
The file was modified	`thys/ROOTS` (diff)