author | chaieb |
Sun, 05 Apr 2009 19:21:51 +0100 | |
changeset 30867 | 6fff6030338b |
parent 30866 | dd5117e2d73e |
child 30868 | 1040425c86a2 |
1.1 --- a/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy Sun Apr 05 05:07:10 2009 +0100 1.2 +++ b/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy Sun Apr 05 19:21:51 2009 +0100 1.3 @@ -3,7 +3,7 @@ 1.4 header {* Examples for Ferrante and Rackoff's quantifier elimination procedure *} 1.5 1.6 theory Dense_Linear_Order_Ex 1.7 -imports Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order" 1.8 +imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" 1.9 begin 1.10 1.11 lemma