lcp = paulson

"code equation" replaces "defining equation"

tuned

improved tackling of subclasses

tuned proof

smart path detection

corrected user aliases

added churn script

Scala wrapper for interactive Isar documents;

added append_list, encode_list; tuned;

join_results: when dependencies are resulved (but not finished yet), always continue execution as worker thread -- improved parallelism at the cost of some reactivity;

with_attributes: make double sure that unsafe attributes are avoided;

bug fixes

bug fixes

improved calculation of morphisms and rules

merged

tuned signature

exported depedencies; tuned signature

merged

merged

use match_tac instead of resolve_tac for continuity simproc

more instance declarations for poly

add lemmas about degree

rename plength to psize

rename divmod_poly to pdivmod

merged.

add strictness and compactness lemmas to Product_Cpo.thy

rename Dsum.thy to Sum_Cpo.thy

minimize dependencies

add lemmas cont2monofunE, cont2cont_apply

add Product_Cpo.thy

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.

merged

bug fix

merged

code cleanup

explicit equation morphism

close derivation of classrels

no document for HOL-Base

moved message markup into Scala layer -- reduced redundancy;

added parse_body_failsafe;

define_state: use empty_state; edit_document: report_updates before running commands; tuned;

provide end_document;

merged

run command: check theory name for init; tuned;

run_command: check theory name for init;

export check_name;

fixed location of Imperative_HOL

adapted to changes in class package

merged

migrated class package to new locale implementation

corrected preparation of instances: parameters are proper names, not raw terms

migrated class package to new locale implementation

merged

fold_entries: non-optional start, permissive; renamed find_entries to first_entry, tuned; update_state: run as state_id'; update_states: symmetric changes;

Result.toString: XML output of status messages;

added HOL-Base image

moved Univ_Poly to Library

merged

tuned

added cert_read_declaration; more exports; tuned signature

merged

command 'Isar.edit_document': actually invoke edit_document;

merged

fixed error message spacing

tuned interpretation code

tuned

type constraints and sort intersection

dropped $Id$

decativate Toplevel.debug after reading

exported break reference

tuned;

edit_document: proper edits/edit markup, including the document id; tuned;

replaced command_state by edits/edit;

removed junk;

merged

one more [code del] declaration

misc cleanup and simplification;

added run_command (from isar_document.ML); tuned;

added command_state markup;

tuned ASCII art;

declare pCons_0_0 [code post]

merged

code generation for polynomials

merged

more [code del] declarations

declare more definitions [code del]

define polynomial multiplication using poly_rec

merged.

declare smult rules [simp]

simplify proof of coeff_mult_degree_sum

convert Deriv.thy to use new Polynomial library (incomplete)

Integration imports ATP_Linkup (for metis)

misc internal rearrangements; fold_entries: really start from start, or optional position; added find_first_entries, find_first_entries; insert_entry: always invalidate next state; added refresh_states (partial version);

replaced sys_error by plain error; some basic operations on command entries within a document;

merged