src/HOL/Mutabelle/ROOT.ML
author himmelma
Tue, 02 Mar 2010 09:57:49 +0100
changeset 35540 3d073a3e1c61
parent 35325 4123977b469d
permissions -rw-r--r--
the ordering on real^1 is linear


use_thy "MutabelleExtra";