added joinable;
authorwenzelm
Wed Jun 29 15:13:23 2005 +0200 (2005-06-29)
changeset 165945d73fbf4eb1e
parent 16593 0115764233e4
child 16595 e64fb2cf50cb
added joinable;
src/Pure/context.ML
     1.1 --- a/src/Pure/context.ML	Tue Jun 28 17:56:04 2005 +0200
     1.2 +++ b/src/Pure/context.ML	Wed Jun 29 15:13:23 2005 +0200
     1.3 @@ -39,6 +39,7 @@
     1.4    val check_thy: string -> theory -> theory
     1.5    val eq_thy: theory * theory -> bool
     1.6    val subthy: theory * theory -> bool
     1.7 +  val joinable: theory * theory -> bool
     1.8    val merge: theory * theory -> theory                     (*exception TERM*)
     1.9    val merge_refs: theory_ref * theory_ref -> theory_ref    (*exception TERM*)
    1.10    val self_ref: theory -> theory_ref
    1.11 @@ -279,6 +280,8 @@
    1.12  
    1.13  fun subthy thys = eq_thy thys orelse proper_subthy thys;
    1.14  
    1.15 +fun joinable (thy1, thy2) = subthy (thy1, thy2) orelse subthy (thy2, thy1);
    1.16 +
    1.17  
    1.18  (* theory references *)
    1.19