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 *}