1.1 --- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Sun Mar 13 20:56:00 2011 +0100
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Sun Mar 13 21:21:48 2011 +0100
     1.3 @@ -1,5 +1,5 @@
     1.4  theory Code_Prolog_Examples
     1.5 -imports Code_Prolog
     1.6 +imports "~~/src/HOL/Library/Code_Prolog"
     1.7  begin
     1.8  
     1.9  section {* Example append *}

     2.1 --- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Sun Mar 13 20:56:00 2011 +0100
     2.2 +++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Sun Mar 13 21:21:48 2011 +0100
     2.3 @@ -1,5 +1,5 @@
     2.4  theory Context_Free_Grammar_Example
     2.5 -imports Code_Prolog
     2.6 +imports "~~/src/HOL/Library/Code_Prolog"
     2.7  begin
     2.8  
     2.9  declare mem_def[code_pred_inline]

     3.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Sun Mar 13 20:56:00 2011 +0100
     3.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Sun Mar 13 21:21:48 2011 +0100
     3.3 @@ -1,5 +1,8 @@
     3.4  theory Hotel_Example_Prolog
     3.5 -imports Hotel_Example "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs" Code_Prolog
     3.6 +imports
     3.7 +  Hotel_Example
     3.8 +  "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
     3.9 +  "~~/src/HOL/Library/Code_Prolog"
    3.10  begin
    3.11  
    3.12  declare Let_def[code_pred_inline]

     4.1 --- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Sun Mar 13 20:56:00 2011 +0100
     4.2 +++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Sun Mar 13 21:21:48 2011 +0100
     4.3 @@ -1,5 +1,5 @@
     4.4  theory Lambda_Example
     4.5 -imports Code_Prolog
     4.6 +imports "~~/src/HOL/Library/Code_Prolog"
     4.7  begin
     4.8  
     4.9  subsection {* Lambda *}

     5.1 --- a/src/HOL/Predicate_Compile_Examples/List_Examples.thy	Sun Mar 13 20:56:00 2011 +0100
     5.2 +++ b/src/HOL/Predicate_Compile_Examples/List_Examples.thy	Sun Mar 13 21:21:48 2011 +0100
     5.3 @@ -1,5 +1,8 @@
     5.4  theory List_Examples
     5.5 -imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck" "Code_Prolog"
     5.6 +imports
     5.7 +  Main
     5.8 +  "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
     5.9 +  "~~/src/HOL/Library/Code_Prolog"
    5.10  begin
    5.11  
    5.12  setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *}

     6.1 --- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Sun Mar 13 20:56:00 2011 +0100
     6.2 +++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Sun Mar 13 21:21:48 2011 +0100
     6.3 @@ -1,5 +1,7 @@
     6.4  theory Reg_Exp_Example
     6.5 -imports "~~/src/HOL/Library/Predicate_Compile_Quickcheck" Code_Prolog
     6.6 +imports
     6.7 +  "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
     6.8 +  "~~/src/HOL/Library/Code_Prolog"
     6.9  begin
    6.10  
    6.11  text {* An example from the experiments from SmallCheck (http://www.cs.york.ac.uk/fp/smallcheck/) *}