[isabelle] Changes in inductive tactics



Hi,

I have noticed that the Isabelle function 'Induct.induct_tac' has changed its signature from

  val induct_tac: Proof.context -> (binding option * term) option list list ->
    (string * typ) list list -> term option list -> thm list option ->
    thm list -> int -> cases_tactic

to

  val induct_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
    (string * typ) list list -> term option list -> thm list option ->
    thm list -> int -> cases_tactic

in the new Isabelle release 2009-2. However, I could not tell from the source code what are the bool on the second argument and the bools paired to the terms on the third argument.
Does anybody know how they are used?

Best regards,
Omar.


-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.