src/Cube/LOmega.thy
author oheimb
Wed, 25 Feb 1998 20:25:27 +0100
changeset 4652 d24cca140eeb
parent 4583 6d9be46ea566
permissions -rw-r--r--
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning combination of classical reasoner and simplifier auto_tac into Provers/clasimp.ML explicitly introducing combined type clasimpset


LOmega = L2 + Lomega