(* Title: Regular Algebras Author: Simon Foster, Georg Struth Maintainer: Simon Foster <s.foster at york.ac.uk> Georg Struth <g.struth at sheffield.ac.uk> *) section ‹Pratt's Counterexamples› theory Pratts_Counterexamples imports Regular_Algebras begin text ‹We create two regular algebra models due to Pratt~\<^cite>‹"Pratt"› which are used to distinguish K1 algebras from K1l and K1r algebras.›