2008-01-29 huffman 2008-01-29 new term-building combinators
2008-01-29 haftmann 2008-01-29 cleaned up evaluation interfaces
2008-01-29 haftmann 2008-01-29 tuned names
2008-01-29 haftmann 2008-01-29 treating division by zero properly
2008-01-28 wenzelm 2008-01-28 eliminated escaped white space;
2008-01-28 wenzelm 2008-01-28 basic scanners: produce symbol list instead of imploded string; tuned signature;
2008-01-28 wenzelm 2008-01-28 * Outer syntax: string tokens no longer admit escaped white space;
2008-01-28 wenzelm 2008-01-28 location_of_position: Position.column_of (which counts Isabelle symbols, not characters);
2008-01-28 wenzelm 2008-01-28 added count/counted: improved position handling for token syntax; removed obsolete incr_line/keep_line/scan_blank; string tokens no longer admit escaped white space, which was an accidental (undocumented) feature;
2008-01-28 wenzelm 2008-01-28 added column field; replaced inc by general advance operation; str_of: no output for file without line information;
2008-01-28 wenzelm 2008-01-28 T.count/counted: improved position handling for token syntax;
2008-01-28 wenzelm 2008-01-28 added column property;
2008-01-28 wenzelm 2008-01-28 removed redundant repeatd scanner combinator;
2008-01-28 wenzelm 2008-01-28 added ::: / @@@ scanner combinators;
2008-01-28 berghofe 2008-01-28 Tuned uniqueness proof for recursion combinator.
2008-01-28 berghofe 2008-01-28 Cleaned up simproc code.
2008-01-28 urbanc 2008-01-28 tuned the proof of the substitution lemma
2008-01-27 wenzelm 2008-01-27 rename_client_map_tac: avoid ill-defined thm reference;
2008-01-27 wenzelm 2008-01-27 use_thy: do not set implicit ML context anymore;
2008-01-27 wenzelm 2008-01-27 added ambiguity_limit (restricts parse trees / terms printed in messages); tuned;
2008-01-27 wenzelm 2008-01-27 renamed thms_containing_limit to FindTheorems.limit;
2008-01-27 wenzelm 2008-01-27 eliminated some legacy ML files;
2008-01-27 wenzelm 2008-01-27 added bind_thms;
2008-01-27 wenzelm 2008-01-27 tuned;
2008-01-27 wenzelm 2008-01-27 removed legacy ML file;
2008-01-26 wenzelm 2008-01-26 syntax error: unified output of priorities;
2008-01-26 wenzelm 2008-01-26 syntax error: reduced spam -- print expected nonterminals instead of terminals; tuned pretty_gram;
2008-01-26 wenzelm 2008-01-26 avoid redundant escaping of Isabelle symbols;
2008-01-26 wenzelm 2008-01-26 grouped versions of axioms/define/notes;
2008-01-26 wenzelm 2008-01-26 misc tuning and internal rearrangement; tuned attribute syntax -- no need for eta-expansion;
2008-01-26 wenzelm 2008-01-26 added theorem group property;
2008-01-26 wenzelm 2008-01-26 added theorem group operations; note_thmss: add kind to *all* intermediate thms; get_kind: default to empty name;
2008-01-26 wenzelm 2008-01-26 added surround;
2008-01-26 wenzelm 2008-01-26 tuned attribute syntax -- no need for eta-expansion;
2008-01-26 wenzelm 2008-01-26 added theorem group;
2008-01-26 wenzelm 2008-01-26 internal inductive: fresh theorem group;
2008-01-25 wenzelm 2008-01-25 modernized primrec;
2008-01-25 wenzelm 2008-01-25 Codegenerator vs. Codegenerator_Pretty: loaded sequentially, due to hazardous ML sections; more simultaneous use_thys;
2008-01-25 wenzelm 2008-01-25 modernized primrec;
2008-01-25 wenzelm 2008-01-25 tuned document; modernized primrec;
2008-01-25 wenzelm 2008-01-25 tuned document;
2008-01-25 wenzelm 2008-01-25 tuned;
2008-01-25 wenzelm 2008-01-25 * Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs here;
2008-01-25 haftmann 2008-01-25 tuned
2008-01-25 haftmann 2008-01-25 print postprocessor equations
2008-01-25 haftmann 2008-01-25 fixed and tuned
2008-01-25 haftmann 2008-01-25 dropped superfluous code theorems
2008-01-25 haftmann 2008-01-25 improved code theorem setup
2008-01-25 haftmann 2008-01-25 consistent interacitve bootstrap of HOL-Main
2008-01-25 haftmann 2008-01-25 distinguished examples for Efficient_Nat.thy
2008-01-25 haftmann 2008-01-25 clarified setup of method "normalization"
2008-01-25 haftmann 2008-01-25 moved definition of power on ints to theory Int
2008-01-24 wenzelm 2008-01-24 removed unused properties; replaced ContextPosition by Position.thread_data;
2008-01-24 wenzelm 2008-01-24 replaced ContextPosition by Position.thread_data;
2008-01-24 wenzelm 2008-01-24 statement: keep explicit position; replaced ContextPosition by Position.thread_data;
2008-01-24 wenzelm 2008-01-24 improved apply: handle thread position, apply to context here; replaced ContextPosition by Position.thread_position;
2008-01-24 wenzelm 2008-01-24 removed unused Toplevel.properties;
2008-01-24 wenzelm 2008-01-24 added combinator for wrapped lazy evaluation;
2008-01-24 wenzelm 2008-01-24 added setmp_thread_data_seq;
2008-01-24 wenzelm 2008-01-24 removed obsolete context_position.ML (superseded by Position.thread_data);