src/HOL/UNITY/Comp/Alloc.thy
changeset 21669 c68717c16013
parent 21632 e7c1f1a77d18
child 21710 4e4b7c801142
     1.1 --- a/src/HOL/UNITY/Comp/Alloc.thy	Tue Dec 05 22:14:53 2006 +0100
     1.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy	Wed Dec 06 01:12:36 2006 +0100
     1.3 @@ -288,6 +288,9 @@
     1.4    bij_image_Collect_eq
     1.5  
     1.6  ML {*
     1.7 +local
     1.8 +  val INT_D = thm "INT_D";
     1.9 +in
    1.10  (*Splits up conjunctions & intersections: like CONJUNCTS in the HOL system*)
    1.11  fun list_of_Int th = 
    1.12      (list_of_Int (th RS conjunct1) @ list_of_Int (th RS conjunct2))
    1.13 @@ -295,6 +298,7 @@
    1.14      handle THM _ => (list_of_Int (th RS INT_D))
    1.15      handle THM _ => (list_of_Int (th RS bspec))
    1.16      handle THM _ => [th];
    1.17 +end;
    1.18  *}
    1.19  
    1.20  lemmas lessThanBspec = lessThan_iff [THEN iffD2, THEN [2] bspec]