src/HOL/UNITY/Follows.thy
changeset 41413 64cd30d6b0b8
parent 35416 d8d7d1b785af
child 54859 64ff7f16d5b7
     1.1 --- a/src/HOL/UNITY/Follows.thy	Wed Dec 29 13:51:17 2010 +0100
     1.2 +++ b/src/HOL/UNITY/Follows.thy	Wed Dec 29 17:34:41 2010 +0100
     1.3 @@ -5,7 +5,9 @@
     1.4  
     1.5  header{*The Follows Relation of Charpentier and Sivilotte*}
     1.6  
     1.7 -theory Follows imports SubstAx ListOrder Multiset begin
     1.8 +theory Follows
     1.9 +imports SubstAx ListOrder "~~/src/HOL/Library/Multiset"
    1.10 +begin
    1.11  
    1.12  definition Follows :: "['a => 'b::{order}, 'a => 'b::{order}] => 'a program set" (infixl "Fols" 65) where
    1.13     "f Fols g == Increasing g \<inter> Increasing f Int