[isabelle-dev] NEWS: ML_file

Makarius makarius at sketis.net
Wed Aug 22 23:49:41 CEST 2012

Previous message (by thread): [isabelle-dev] Generated files in Codegen
Next message (by thread): [isabelle-dev] Building nightly snapshots
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

* Command 'ML_file' evaluates ML text from a file directly within the
theory, without any predeclaration via 'uses' in the theory header.


This refers to Isabelle/4cd4ef1ef4a4 and before.


 	Makarius

Previous message (by thread): [isabelle-dev] Generated files in Codegen
Next message (by thread): [isabelle-dev] Building nightly snapshots
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

More information about the isabelle-dev mailing list