[isabelle] Inductive set and tutorial



Dear list, I'm afraid I'm still having troubles with the updated tutorial of http://isabelle.in.tum.de/devel/Isabelle_04-Feb-2009_pdf.tar.gz. Everithing was fine until this example of page 19 of isar-overview.pdf

inductive_set
  rtc :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a)set"   ("_*" [1000] 999)
  for r :: "('a \<times> 'a)set"
where
  refl: "(x,x) \<in> r\<^sup>*"
| step: "\<lbrakk> (x,y) \<in> r; (y,z) \<in> r\<^sup>* \<rbrakk> \<Longrightarrow> (x,z) \<in> r\<^sup>*"

*** Ill-formed introduction rule "refl"
*** r^** x x
*** Conclusion of introduction rule must be an inductive predicate
*** At command "inductive_set".


Any help will be appreciated, regards,

Juan

 -- 
------------------------------------------------------------------------
Juan Rodríguez Hortalá
Grupo de Programación Declarativa / Declarative Programming Group
E-Mail : juanrh at fdi.ucm.es
Home Page: http://gpd.sip.ucm.es/juanrh/
Tel: + 34 913947646
Despacho / Office: 220 (2ª planta / 2nd floor)
Dept. Sistemas Informáticos y Computación / Department of Computer Systems and Computing
Universidad Complutense de Madrid
Facultad de Informática
C/ Profesor José García Santesmases, s/n
E - 28040 Madrid. Spain






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