Re: [isabelle] documentation



Hi Stefania,

> Thank you for the hints but still i didn't solve the error. 
> I looked in log/HOL-StefSession file and the only error i fond is this:
> 
> Loading theory "Abstract"
> val it = () : unit
> val it = () : unit
> ### Browser info: cannot access session index of
> "/home/stefania/isabelle/browser_info/HOL"
> "$ISATOOL" document -c -o 'pdf' -n 'document' -t ''
> '/home/stefania/isabelle/browser_info/HOL/StefSession/document' 2>&1
> This is pdfeTeXk, Version 3.141592-1.21a-2.2 (Web2C 7.5.4)
>  file:line:error style messages enabled.
>  %&-line parsing enabled.

Hmmm... can you send me the log (not via the mailing list please)?

> About the "includes" command. i am using it for example in:
> 
> lemma(in comm_group) :
> includes group G1+ group G2
> assumes ....
> shows...

In that case just use the corresponding locale predicate expressions as
assumptions, e.g. like in lemma subgroup_is_group in
src/HOL/Algebra/Group.thy:

lemma (in comm_group):
  assumes "group G1" and "group G2"
  fixes ...
  assumes ...
  shows ...

Hope this helps,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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