src/HOL/Library/Library/ROOT.ML
changeset 25315 6ff4305d2f7c
parent 24104 719fbe4fb77f
child 26735 39be3c7e643a
equal deleted inserted replaced
25314:5eaf3e8b50a4 25315:6ff4305d2f7c
     1 (* $Id$ *)
     1 (* $Id$ *)
     2 
     2 
     3 use_thys ["Library", "List_Prefix", "List_lexord", "SCT_Examples"];
     3 use_thys ["Library", "List_Prefix", "List_lexord"];