1open HolKernel Parse boolLib bossLib; 2 3open tyabbrevTheory 4 5val _ = new_theory "untyabbrev"; 6 7val _ = Parse.disable_tyabbrev_printing "reln" 8 9 10val _ = export_theory(); 11