CookBook/Package/Ind_Interface.thy
changeset 42 cd612b489504
parent 35 d5c090b9a2b1
child 53 0c3580c831a4
--- a/CookBook/Package/Ind_Interface.thy	Mon Oct 20 06:22:11 2008 +0000
+++ b/CookBook/Package/Ind_Interface.thy	Mon Oct 27 18:48:52 2008 +0100
@@ -1,5 +1,5 @@
 theory Ind_Interface
-imports Base Simple_Inductive_Package
+imports "../Base" Simple_Inductive_Package
 begin
 
 (*<*)
@@ -114,7 +114,7 @@
          Const (\"all\", \<dots>) $ Abs (\"z\", TFree (\"'a\", \<dots>),
            Const (\"==>\", \<dots>) $
              (Const (\"Trueprop\", \<dots>) $
-                (Free (\"trcl\", \<dots>) $ Free (\"r\", \<dots>) $ Bound 2 $ Bound 1)) $
+               (Free (\"trcl\", \<dots>) $ Free (\"r\", \<dots>) $ Bound 2 $ Bound 1)) $
              (Const (\"==>\", \<dots>) $ \<dots> $ \<dots>))))])]),
  \<dots>)
 : (((Name.binding * typ) * mixfix) list *