etc/isar-keywords.el
2006-10-10 haftmann 2006-10-10 added code_abstype and code_constsubst
2006-10-02 haftmann 2006-10-02 normal_form now a diagnostic command
2006-09-25 haftmann 2006-09-25 added code_instname
2006-09-19 haftmann 2006-09-19 code_gen now peek keyword
2006-09-18 wenzelm 2006-09-18 updated;
2006-09-13 krauss 2006-09-13 Major update to function package, including new syntax and the (only theoretical) ability to handle local contexts.
2006-09-01 haftmann 2006-09-01 final syntax for some Isar code generator keywords
2006-08-29 haftmann 2006-08-29 updated keywords
2006-08-14 haftmann 2006-08-14 updated code generator keywords
2006-08-08 haftmann 2006-08-08 added code_constname keyword
2006-08-04 krauss 2006-08-04 Added Keywords: "otherwise" and "sequential", needed for function package's sequential mode.
2006-06-14 haftmann 2006-06-14 keyword update
2006-06-12 haftmann 2006-06-12 updated keywords
2006-06-06 wenzelm 2006-06-06 updated;
2006-05-16 wenzelm 2006-05-16 updated;
2006-05-13 wenzelm 2006-05-13 updated;
2006-05-05 krauss 2006-05-05 First usable version of the new function definition package (HOL/function_packake/...). Moved Accessible_Part.thy from Library to Main.
2006-03-14 wenzelm 2006-03-14 updated;
2006-03-14 wenzelm 2006-03-14 updated;
2006-02-27 haftmann 2006-02-27 added nbe
2006-02-16 wenzelm 2006-02-16 updated;
2006-02-01 wenzelm 2006-02-01 updated;
2006-01-25 wenzelm 2006-01-25 updated;
2006-01-23 haftmann 2006-01-23 removed problematic keyword 'atom'
2006-01-17 haftmann 2006-01-17 substantial improvements in code generator
2006-01-07 wenzelm 2006-01-07 updated;
2006-01-03 haftmann 2006-01-03 class now a keyword
2006-01-03 wenzelm 2006-01-03 updated -- lost update!?
2005-12-29 haftmann 2005-12-29 added atom keyword
2005-12-29 haftmann 2005-12-29 changes in code generator keywords
2005-12-09 haftmann 2005-12-09 substantial improvements for class code generation
2005-12-02 haftmann 2005-12-02 adopted keyword for code generator
2005-11-22 haftmann 2005-11-22 added code generator syntax
2005-11-22 haftmann 2005-11-22 added code generator syntax
2005-11-14 haftmann 2005-11-14 new syntax for class_package
2005-10-15 wenzelm 2005-10-15 updated;
2005-09-21 berghofe 2005-09-21 Added new "value" command.
2005-09-17 wenzelm 2005-09-17 manually generated from Isabelle/HOLCF/IOA/Complex/Import;
2005-09-01 wenzelm 2005-09-01 updated;
2005-08-25 berghofe 2005-08-25 Adapted to new code generator syntax.
2005-08-17 paulson 2005-08-17 new command to invoke ATPs
2005-07-12 berghofe 2005-07-12 Added "attach" keyword for code generator setup.
2005-07-06 huffman 2005-07-06 add keywords cpodef, pcpodef (for HOLCF)
2005-06-17 wenzelm 2005-06-17 updated;
2005-06-04 huffman 2005-06-04 add keywords fixrec and fixpat for HOLCF fixrec package
2005-06-01 ballarin 2005-06-01 Locales: new element constrains, parameter renaming with syntax, experimental command instantiate withdrawn.
2005-05-22 wenzelm 2005-05-22 updated;
2005-04-17 wenzelm 2005-04-17 updated;
2005-04-13 wenzelm 2005-04-13 *** empty log message ***
2005-03-24 ballarin 2005-03-24 Further work on interpretation commands. New command `interpret' for interpretation in proof contexts.
2005-03-10 ballarin 2005-03-10 Registrations of global locale interpretations: improved, better naming.
2005-03-09 ballarin 2005-03-09 First version of global registration command.
2004-12-13 nipkow 2004-12-13 added find_rewrites
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 Added "import" and "begin"
2004-06-13 wenzelm 2004-06-13 updated;
2004-04-23 wenzelm 2004-04-23 updated -- too late for Isabelle2004!
2004-04-02 ballarin 2004-04-02 Experimental command for instantiation of locales in proof contexts: instantiate <label>: <loc>
2004-01-10 webertj 2004-01-10 'refute', 'refute_params'.
2003-10-09 skalberg 2003-10-09 Added support for making constants final, that is, ensuring that no definition can be given later (useful for constants whose behaviour is fixed axiomatically rather than definitionally).