diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 30bd663bb6d935ecc6b42ab11ad07cf18bf0def0..36313df6ce8c335fec3e9480f643ee537fb4048a 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -934,8 +934,16 @@ class visitor (ctx:context) c =
                 let decl = Why3.Decl.create_logic_decl [decl] in
                 ctx.th <- Why3.Theory.add_decl ~warn:false ctx.th decl
           end
-        | Inductive _dl ->
-            why3_failure "inductive definitions not yet implemented"
+        | Inductive dl ->
+            (* create predicate symbol *)
+            let id = Why3.Ident.id_fresh (Qed.Export.link_name (lfun_name d.d_lfun)) in
+            let map e = Why3.Opt.get (of_tau ~cnv (Lang.F.tau_of_var e)) in
+            let ty_args = List.map map d.d_params in
+            let id = Why3.Term.create_lsymbol id ty_args None in
+            let decl = Why3.Decl.create_param_decl id in
+            ctx.th <- Why3.Theory.add_decl ~warn:false ctx.th decl ;
+            (* register axioms *)
+            List.iter (self#on_dlemma) dl
       end
 
   end