equal
deleted
inserted
replaced
1 no_document use_thys ["Code_Integer"]; |
1 no_document use_thys ["~~/src/HOL/Library/Code_Integer"]; |
2 use_thys ["Eta", "StrongNorm", "Standardization", "WeakNorm"]; |
2 use_thys ["Eta", "StrongNorm", "Standardization", "WeakNorm"]; |