2005-07-01 wenzelm 2005-07-01 low-level tuning of fold, fold_rev, foldl_map;
2005-07-01 wenzelm 2005-07-01 isatool install: removed KDE option;
2005-07-01 berghofe 2005-07-01 Fixed bug: lookup' must use = instead of eq_type to compare types of variables, otherwise pattern matching algorithm may loop.
2005-07-01 berghofe 2005-07-01 Changed interface of Envir.lookup'
2005-07-01 berghofe 2005-07-01 Moved eq_type from envir.ML to type.ML
2005-07-01 berghofe 2005-07-01 Implemented modular code generation.
2005-07-01 berghofe 2005-07-01 Simplified proof (thanks to strengthened ball_cong).
2005-07-01 berghofe 2005-07-01 Proof of wx_ex_prop must now use old bex_cong to prevent simplifier from looping.
2005-07-01 berghofe 2005-07-01 Adapted to new interface of RecfunCodegen.add.
2005-07-01 berghofe 2005-07-01 Adapted to modular code generation.
2005-07-01 berghofe 2005-07-01 Corrected implementation of arbitrary on cname.
2005-07-01 berghofe 2005-07-01 Added BasisLibrary prefix to List.concat to avoid problems with modular code generation.
2005-07-01 berghofe 2005-07-01 Moved code generator setup from NatBin to IntDef.
2005-07-01 berghofe 2005-07-01 Simplified some proofs (thanks to strong_setsum_cong).
2005-07-01 berghofe 2005-07-01 Removed setsubgoaler hack (thanks to strong_setsum_cong).
2005-07-01 berghofe 2005-07-01 Removed setsubgoaler hack (thanks to strengthened finsum_cong).
2005-07-01 berghofe 2005-07-01 Removed setsubgoaler hack.
2005-07-01 berghofe 2005-07-01 Tuned finsum_cong to allow that premises are simplified more eagerly.
2005-07-01 berghofe 2005-07-01 Added strong_ball_cong and strong_bex_cong (these are now the standard congruence rules for Ball and Bex).
2005-07-01 berghofe 2005-07-01 Moved some code lemmas from Main to Nat.
2005-07-01 berghofe 2005-07-01 Adapted to new interface of code generator.
2005-07-01 berghofe 2005-07-01 Implemented trick (due to Tobias Nipkow) for fine-tuning simplification of premises of congruence rules.
2005-07-01 berghofe 2005-07-01 Added strong_setsum_cong and strong_setprod_cong.
2005-07-01 huffman 2005-07-01 defaultsort pcpo
2005-07-01 huffman 2005-07-01 added theorem lift_definedE; moved cont_if to Cont.thy
2005-07-01 huffman 2005-07-01 added tactic cont_tac
2005-07-01 huffman 2005-07-01 remove uses of sign_of
2005-07-01 huffman 2005-07-01 cleaned up
2005-07-01 huffman 2005-07-01 cleaned up
2005-07-01 huffman 2005-07-01 renamed flatdom2monofun to flatdom_strict2mono
2005-07-01 huffman 2005-07-01 cleaned up; reorganized and added section headings
2005-07-01 huffman 2005-07-01 cleaned up; added adm_less to adm_lemmas; added subsection headings
2005-06-30 wenzelm 2005-06-30 revert to 1.27 due to obscure performance issues (!??);
2005-06-30 huffman 2005-06-30 replace filter2 with List.partition
2005-06-30 ballarin 2005-06-30 Proper treatment of beta-redexes in witness theorems.
2005-06-30 haftmann 2005-06-30 minor corrections
2005-06-30 kleing 2005-06-30 test sml-dev on mac as well
2005-06-30 kleing 2005-06-30 use only 1 CPU on MacOS 10.4.1
2005-06-30 kleing 2005-06-30 use kleing@cse instead of kleing@in.tum.de
2005-06-30 kleing 2005-06-30 use global settings for isatest-doc
2005-06-29 wenzelm 2005-06-29 export no_type_brackets; accomodate advanced trfuns; tuned;
2005-06-29 wenzelm 2005-06-29 proper treatment of advanced trfuns: pass thy argument; tuned warning;
2005-06-29 wenzelm 2005-06-29 transform_failure in translation functions: TRANSLATION_FAIL; proper treatment of advanced trfuns: pass thy argument; tuned bigimpl_ast_tr, impl_ast_tr';
2005-06-29 wenzelm 2005-06-29 proper treatment of advanced trfuns: pass thy argument; transform_failure in translation functions: TRANSLATION_FAIL; removed obsolete '*** INSUFFICIENT SYNTAX FOR PREFIX APPLICATION ***';
2005-06-29 wenzelm 2005-06-29 accomodate advanced trfuns;
2005-06-29 wenzelm 2005-06-29 removed obsolete (un)fold_ast2;
2005-06-29 wenzelm 2005-06-29 Drule.implies_intr_hyps;
2005-06-29 wenzelm 2005-06-29 added print': print depending on print_mode;
2005-06-29 wenzelm 2005-06-29 no Syntax.internal on thesis;
2005-06-29 wenzelm 2005-06-29 added print_mode three_buffersN and corresponding cond_print;
2005-06-29 wenzelm 2005-06-29 cond_print for end-of-proof and calculational commands;
2005-06-29 wenzelm 2005-06-29 added eq; improved copy/copy_dir: only copy if non-eq;
2005-06-29 wenzelm 2005-06-29 pass thy as explicit argument (the old ref was not safe in conjunction with lazy evaluation -- the unify code could be fooled about the present theory context);
2005-06-29 wenzelm 2005-06-29 more efficient treatment of shyps and hyps (use ordered lists); added 'sorts' field to cterm; removed obsolete fix_shyps; moved implies_intr_hyps to drule.ML;
2005-06-29 wenzelm 2005-06-29 Syntax.read thy;
2005-06-29 wenzelm 2005-06-29 tuned sort_ord: pointer_eq; tuned size_of_term: less stack usage;
2005-06-29 wenzelm 2005-06-29 removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort; added efficient operations on ordered lists: eq_set, union, subtract, insert_sort/typ(s)/term(s);
2005-06-29 wenzelm 2005-06-29 eliminated separate syn type -- advanced trfuns already part of Syntax.syntax;
2005-06-29 wenzelm 2005-06-29 replaced Syntax.simple_pprint_typ by (Sign.pprint_typ ProtoPure.thy);
2005-06-29 wenzelm 2005-06-29 added implies_intr_hyps (from thm.ML);