src/HOL/MiniML/ROOT.ML
changeset 1925 1150f128c7fe
parent 1351 4a960c012383
child 2031 03a843f0f447
--- a/src/HOL/MiniML/ROOT.ML	Tue Aug 20 12:23:13 1996 +0200
+++ b/src/HOL/MiniML/ROOT.ML	Tue Aug 20 12:32:16 1996 +0200
@@ -11,4 +11,6 @@
 writeln"Root file for HOL/MiniML";
 Unify.trace_bound := 20;
 
+AddSEs [less_SucE];
+
 time_use_thy "I";