Re: [isabelle] Monad_Syntax latex symbols



> Isabelle provides infinitely many symbols, but only a finite list of
> well-known ones are defined in the default LaTeX styles.  This is done in
> a way that avoids conflicts of LaTeX packages, i.e. isabellesym.sty does
> not force any packages on the user.

OK

> > thm (do_notation) Ref.change_def
> > text {* @{thm [mode=do_notation] Ref.change_def} *}
> > ----------
> > 
> > Could this mode be set in a global way to be used by default in
> > antiquotations? and also in proofs?
> 
> This is the normal Isabelle "print mode".  You can modify it in some
> command line tools like "usedir" using option -m, for example.  For
> document preparation there is a global default Thy_Output.modes, which can
> be set in ROOT.ML.

OK, I think these are the good way to do it:

- for document preparation in ROOT.ML:
Unsynchronized.change Thy_Output.modes (insert (op =) "do_notation");

- for display:
ML{* Unsynchronized.change print_mode (insert (op =) "do_notation") *}


To be able to have some exceptions, I have also added an other option to 
antiquotations:

----------
fun without_modes modes f x =
  let val modes' = subtract (op =) modes (Print_Mode.print_mode_value ())
  in Print_Mode.setmp modes' f x end;

val _ = Thy_Output.add_option "rmmode"
  (Thy_Output.add_wrapper o without_modes o single);
----------

Thanks,

Mathieu





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