# HG changeset patch
# User bulwahn
# Date 1270046681 -7200
# Node ID 93d62439506c0ea5b495717376995fe4aed52efc
# Parent  29e242e9e9a36bbe2d90ea800fa1ee8c4531fe86
adopting specialisation examples to moving the alternative defs in the library

diff -r 29e242e9e9a3 -r 93d62439506c src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Wed Mar 31 16:44:41 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Wed Mar 31 16:44:41 2010 +0200
@@ -1,5 +1,5 @@
 theory Specialisation_Examples
-imports Main "../ex/Predicate_Compile_Alternative_Defs"
+imports Main Predicate_Compile_Alternative_Defs
 begin
 
 section {* Specialisation Examples *}