changeset 32308 | c2b74affab85 |
parent 31225 | df6945ac4193 |
child 32318 | bca7fd849829 |
--- a/src/HOL/ex/Predicate_Compile.thy Tue Aug 04 08:34:56 2009 +0200 +++ b/src/HOL/ex/Predicate_Compile.thy Tue Aug 04 08:34:56 2009 +0200 @@ -1,5 +1,5 @@ theory Predicate_Compile -imports Complex_Main Lattice_Syntax Code_Eval +imports Complex_Main Lattice_Syntax Code_Eval RPred uses "predicate_compile.ML" begin