| author | bulwahn | 
| Wed, 24 Mar 2010 17:40:44 +0100 | |
| changeset 35954 | d87d85a5d9ab | 
| parent 35953 | 0460ff79bb52 | 
| child 35955 | e657fb805c68 | 
| src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy | file | annotate | diff | comparison | revisions | 
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Wed Mar 24 17:40:43 2010 +0100 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Wed Mar 24 17:40:44 2010 +0100 @@ -1,5 +1,5 @@ theory Predicate_Compile_Examples -imports "../ex/Predicate_Compile_Alternative_Defs" +imports Predicate_Compile_Alternative_Defs begin subsection {* Basic predicates *}