2012-04-05 wenzelm 2012-04-05 less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;
2012-04-05 wenzelm 2012-04-05 more explicit memo_eval vs. memo_result, to enforce bottom-up execution; edit of perspective touches node superficially, to ensure revisit after update;
2012-04-05 wenzelm 2012-04-05 Command.memo including physical interrupts (unlike Lazy.lazy); re-assign unstable exec, i.e. reset interrupted transaction; node result as direct exec -- avoid potential interrupt instability of Lazy.map;
2012-04-05 wenzelm 2012-04-05 tuned;
2012-04-04 wenzelm 2012-04-04 tuned -- NB: get_theory still needs to apply Lazy.force due to interrupt instabilities;
2012-04-04 wenzelm 2012-04-04 proper signature constraint;
2012-04-04 wenzelm 2012-04-04 tuned comments;
2012-04-04 wenzelm 2012-04-04 separate module for prover command execution;
2012-04-04 wenzelm 2012-04-04 tuned;
2012-04-04 huffman 2012-04-04 fix typo in ML structure name
2012-04-04 wenzelm 2012-04-04 removed obsolete isar-overview manual;
2012-04-04 sultana 2012-04-04 dealing with SMLNJ errors 'value type in structure doesn't match signature spec' (which originated from lack of type generalisation) and 'unresolved flex record' wrt tptp_interpret
2012-04-04 bulwahn 2012-04-04 merged
2012-04-04 bulwahn 2012-04-04 rudimentary handling of products in finitize_functions in Quickcheck-Narrowing
2012-04-04 bulwahn 2012-04-04 improved equality check for modes in predicate compiler
2012-04-04 huffman 2012-04-04 rename ML structure to avoid shadowing earlier name
2012-04-04 huffman 2012-04-04 add type annotations to make SML happy (cf. ec6187036495)
2012-04-03 huffman 2012-04-03 merged
2012-04-03 huffman 2012-04-03 new transfer proof method
2012-04-03 huffman 2012-04-03 renamed Tools/transfer.ML to Tools/legacy_transfer.ML
2012-04-03 wenzelm 2012-04-03 prefer prog-prove, suppress isar-overview;
2012-04-03 wenzelm 2012-04-03 merged
2012-04-03 wenzelm 2012-04-03 merged
2012-04-03 wenzelm 2012-04-03 formal integration of "prog-prove" manual; "main" is a reference manual;
2012-04-03 wenzelm 2012-04-03 prefer static dependencies;
2012-04-03 huffman 2012-04-03 merged
2012-04-03 huffman 2012-04-03 modernized obsolete old-style theory name with proper new-style underscore
2012-04-03 sultana 2012-04-03 removed use of CharVector in generated parser, to make SMLNJ happy
2012-04-03 wenzelm 2012-04-03 avoid duplicate PIDE markup; tuned;
2012-04-03 wenzelm 2012-04-03 less intrusive visibility;
2012-04-03 wenzelm 2012-04-03 more robust re-import wrt. non-HHF assumptions;
2012-04-03 wenzelm 2012-04-03 consider polyml-5.3.0 as "experimental" since it chokes on HOL-Codegenerator_Test, while 5.2.1 happens to work;
2012-04-03 wenzelm 2012-04-03 close context elements via Expression.cert/read_declaration; ensure visible context;
2012-04-03 wenzelm 2012-04-03 merged
2012-04-03 sultana 2012-04-03 added me to isatest email list
2012-04-03 kuncar 2012-04-03 new package Lifting - initial commit
2012-04-03 huffman 2012-04-03 add floor/ceiling lemmas suggested by René Thiemann
2012-04-03 nipkow 2012-04-03 made sure that " is shown in tutorial text
2012-04-02 Christian Urban 2012-04-02 merged
2012-04-02 Christian Urban 2012-04-02 tuned proofs
2012-04-02 nipkow 2012-04-02 merged
2012-04-02 nipkow 2012-04-02 towards showing " in the tutorial
2012-04-02 Christian Urban 2012-04-02 tuned proof in order to avoid warning message
2012-04-02 huffman 2012-04-02 remove unnecessary qualifiers on names
2012-04-02 huffman 2012-04-02 add lemma Suc_1
2012-04-02 berghofe 2012-04-02 merged
2012-04-02 berghofe 2012-04-02 Require "For" keyword to be followed by at least one whitespace, to avoid that identifiers starting with "For" are interpreted as traceability information
2012-04-03 wenzelm 2012-04-03 normalize defs (again, cf. 008b7858f3c0);
2012-04-03 wenzelm 2012-04-03 some context examples;
2012-04-03 wenzelm 2012-04-03 retain literal non-HHF assumptions, to facilitate re-import in Generic_Target.import_export_proof;
2012-04-03 wenzelm 2012-04-03 another attempt to avoid duplication of global vs. local syntax (reminiscent of old fork_mixfix);
2012-04-03 wenzelm 2012-04-03 export into target context (again), to retain its 'defines' (e.g. abbreviation lcoeff in theory HOL/Algebra/UnivPoly);
2012-04-03 wenzelm 2012-04-03 better drop background syntax if entity depends on parameters; more direct Type_Infer_Context.const_type instead of Syntax.check_term, which expands abbreviations (and potentially more);
2012-04-03 wenzelm 2012-04-03 more uniform abbrev vs. define;
2012-04-03 wenzelm 2012-04-03 tuned;
2012-04-03 wenzelm 2012-04-03 clarified generic_const vs. close_schematic_term;
2012-04-03 wenzelm 2012-04-03 tuned;
2012-04-03 wenzelm 2012-04-03 more uniform theory_abbrev with const_declaration;
2012-04-03 wenzelm 2012-04-03 avoid const_declaration in aux. context (cf. locale_foundation);
2012-04-03 wenzelm 2012-04-03 clarified background_foundation vs. theory_foundation (with const_declaration);