2009-01-19 haftmann 2009-01-19 improved tackling of subclasses
2009-01-19 haftmann 2009-01-19 tuned proof
2009-01-18 haftmann 2009-01-18 smart path detection
2009-01-18 haftmann 2009-01-18 corrected user aliases
2009-01-18 haftmann 2009-01-18 added churn script
2009-01-18 wenzelm 2009-01-18 Scala wrapper for interactive Isar documents;
2009-01-18 wenzelm 2009-01-18 added append_list, encode_list; tuned;
2009-01-18 wenzelm 2009-01-18 join_results: when dependencies are resulved (but not finished yet), always continue execution as worker thread -- improved parallelism at the cost of some reactivity;
2009-01-18 wenzelm 2009-01-18 with_attributes: make double sure that unsafe attributes are avoided;
2009-01-18 nipkow 2009-01-18 bug fixes
2009-01-18 nipkow 2009-01-18 bug fixes
2009-01-18 haftmann 2009-01-18 improved calculation of morphisms and rules
2009-01-17 haftmann 2009-01-17 merged
2009-01-17 haftmann 2009-01-17 tuned signature
2009-01-17 haftmann 2009-01-17 exported depedencies; tuned signature
2009-01-17 huffman 2009-01-17 merged
2009-01-16 huffman 2009-01-16 merged
2009-01-15 huffman 2009-01-15 use match_tac instead of resolve_tac for continuity simproc
2009-01-15 huffman 2009-01-15 more instance declarations for poly
2009-01-15 huffman 2009-01-15 add lemmas about degree
2009-01-15 huffman 2009-01-15 rename plength to psize
2009-01-15 huffman 2009-01-15 rename divmod_poly to pdivmod
2009-01-15 huffman 2009-01-15 merged.
2009-01-15 huffman 2009-01-15 add strictness and compactness lemmas to Product_Cpo.thy
2009-01-14 huffman 2009-01-14 rename Dsum.thy to Sum_Cpo.thy
2009-01-14 huffman 2009-01-14 minimize dependencies
2009-01-14 huffman 2009-01-14 add lemmas cont2monofunE, cont2cont_apply
2009-01-14 huffman 2009-01-14 add Product_Cpo.thy
2009-01-14 huffman 2009-01-14 change to simpler, more extensible continuity simproc define attribute [cont2cont] for continuity rules; new continuity simproc just applies cont2cont rules repeatedly; split theory Product_Cpo from Cprod, so Cfun can import Product_Cpo; add lemma cont2cont_LAM', which is suitable as a cont2cont rule.
2009-01-17 nipkow 2009-01-17 merged
2009-01-17 nipkow 2009-01-17 bug fix
2009-01-17 haftmann 2009-01-17 merged
2009-01-17 haftmann 2009-01-17 code cleanup
2009-01-17 haftmann 2009-01-17 explicit equation morphism
2009-01-17 haftmann 2009-01-17 close derivation of classrels
2009-01-17 haftmann 2009-01-17 no document for HOL-Base
2009-01-16 wenzelm 2009-01-16 moved message markup into Scala layer -- reduced redundancy;
2009-01-16 wenzelm 2009-01-16 added parse_body_failsafe;
2009-01-16 wenzelm 2009-01-16 define_state: use empty_state; edit_document: report_updates before running commands; tuned;
2009-01-16 wenzelm 2009-01-16 provide end_document;
2009-01-16 wenzelm 2009-01-16 merged
2009-01-16 wenzelm 2009-01-16 run command: check theory name for init; tuned;
2009-01-16 wenzelm 2009-01-16 run_command: check theory name for init;
2009-01-16 wenzelm 2009-01-16 export check_name;
2009-01-16 haftmann 2009-01-16 fixed location of Imperative_HOL
2009-01-16 haftmann 2009-01-16 adapted to changes in class package
2009-01-16 haftmann 2009-01-16 merged
2009-01-16 haftmann 2009-01-16 migrated class package to new locale implementation
2009-01-16 haftmann 2009-01-16 corrected preparation of instances: parameters are proper names, not raw terms
2009-01-16 haftmann 2009-01-16 migrated class package to new locale implementation
2009-01-16 wenzelm 2009-01-16 merged
2009-01-16 wenzelm 2009-01-16 fold_entries: non-optional start, permissive; renamed find_entries to first_entry, tuned; update_state: run as state_id'; update_states: symmetric changes;
2009-01-15 wenzelm 2009-01-15 Result.toString: XML output of status messages;
2009-01-16 haftmann 2009-01-16 added HOL-Base image
2009-01-16 haftmann 2009-01-16 moved Univ_Poly to Library
2009-01-16 haftmann 2009-01-16 merged
2009-01-16 haftmann 2009-01-16 tuned
2009-01-16 haftmann 2009-01-16 added cert_read_declaration; more exports; tuned signature
2009-01-15 wenzelm 2009-01-15 merged
2009-01-15 wenzelm 2009-01-15 command 'Isar.edit_document': actually invoke edit_document;