equal
deleted
inserted
replaced
101 xs = ys orelse (subset_stamp (xs, ys) andalso subset_stamp (ys, xs)); |
101 xs = ys orelse (subset_stamp (xs, ys) andalso subset_stamp (ys, xs)); |
102 |
102 |
103 fun is_draft (Sg {stamps = ref "#" :: _, ...}) = true |
103 fun is_draft (Sg {stamps = ref "#" :: _, ...}) = true |
104 | is_draft _ = false; |
104 | is_draft _ = false; |
105 |
105 |
106 fun subsig (Sg{stamps=s1,...}, Sg{stamps=s2,...}) = subset_stamp(s1,s2); |
106 fun subsig (Sg{stamps=s1,...}, Sg{stamps=s2,...}) = |
|
107 s1 = s2 orelse subset_stamp (s1, s2); |
107 |
108 |
108 fun eq_sg (Sg{stamps=s1,...}, Sg{stamps=s2,...}) = eq_set_stamp(s1,s2); |
109 fun eq_sg (Sg{stamps=s1,...}, Sg{stamps=s2,...}) = eq_set_stamp(s1,s2); |
109 |
110 |
110 (* test if same theory names are contained in signatures' stamps, |
111 (* test if same theory names are contained in signatures' stamps, |
111 i.e. if signatures belong to same theory but not necessarily to the same |
112 i.e. if signatures belong to same theory but not necessarily to the same |