2005-07-01 ago berghofe Moved eq_type from envir.ML to type.ML
2005-07-01 ago berghofe Implemented modular code generation.
2005-07-01 ago berghofe Simplified proof (thanks to strengthened ball_cong).
2005-07-01 ago berghofe Proof of wx_ex_prop must now use old bex_cong to prevent simplifier from looping.
2005-07-01 ago berghofe Adapted to new interface of RecfunCodegen.add.
2005-07-01 ago berghofe Adapted to modular code generation.
2005-07-01 ago berghofe Corrected implementation of arbitrary on cname.
2005-07-01 ago berghofe Added BasisLibrary prefix to List.concat to avoid problems with
2005-07-01 ago berghofe Moved code generator setup from NatBin to IntDef.
2005-07-01 ago berghofe Simplified some proofs (thanks to strong_setsum_cong).
2005-07-01 ago berghofe Removed setsubgoaler hack (thanks to strong_setsum_cong).
2005-07-01 ago berghofe Removed setsubgoaler hack (thanks to strengthened finsum_cong).
2005-07-01 ago berghofe Removed setsubgoaler hack.
2005-07-01 ago berghofe Tuned finsum_cong to allow that premises are simplified more eagerly.
2005-07-01 ago berghofe Added strong_ball_cong and strong_bex_cong (these are now the standard
2005-07-01 ago berghofe Moved some code lemmas from Main to Nat.
2005-07-01 ago berghofe Adapted to new interface of code generator.
2005-07-01 ago berghofe Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
2005-07-01 ago berghofe Added strong_setsum_cong and strong_setprod_cong.
2005-07-01 ago huffman defaultsort pcpo
2005-07-01 ago huffman added theorem lift_definedE; moved cont_if to Cont.thy
2005-07-01 ago huffman added tactic cont_tac
2005-07-01 ago huffman remove uses of sign_of
2005-07-01 ago huffman cleaned up
2005-07-01 ago huffman cleaned up
2005-07-01 ago huffman renamed flatdom2monofun to flatdom_strict2mono
2005-07-01 ago huffman cleaned up; reorganized and added section headings
2005-07-01 ago huffman cleaned up; added adm_less to adm_lemmas; added subsection headings
2005-06-30 ago wenzelm revert to 1.27 due to obscure performance issues (!??);
2005-06-30 ago huffman replace filter2 with List.partition
2005-06-30 ago ballarin Proper treatment of beta-redexes in witness theorems.
2005-06-30 ago haftmann minor corrections
2005-06-30 ago kleing test sml-dev on mac as well
2005-06-30 ago kleing use only 1 CPU on MacOS 10.4.1
2005-06-30 ago kleing use kleing@cse instead of kleing@in.tum.de
2005-06-30 ago kleing use global settings for isatest-doc
2005-06-29 ago wenzelm export no_type_brackets;
2005-06-29 ago wenzelm proper treatment of advanced trfuns: pass thy argument;
2005-06-29 ago wenzelm transform_failure in translation functions: TRANSLATION_FAIL;
2005-06-29 ago wenzelm proper treatment of advanced trfuns: pass thy argument;
2005-06-29 ago wenzelm accomodate advanced trfuns;
2005-06-29 ago wenzelm removed obsolete (un)fold_ast2;
2005-06-29 ago wenzelm Drule.implies_intr_hyps;
2005-06-29 ago wenzelm added print': print depending on print_mode;
2005-06-29 ago wenzelm no Syntax.internal on thesis;
2005-06-29 ago wenzelm added print_mode three_buffersN and corresponding cond_print;
2005-06-29 ago wenzelm cond_print for end-of-proof and calculational commands;
2005-06-29 ago wenzelm added eq;
2005-06-29 ago wenzelm pass thy as explicit argument (the old ref was not safe
2005-06-29 ago wenzelm more efficient treatment of shyps and hyps (use ordered lists);
2005-06-29 ago wenzelm Syntax.read thy;
2005-06-29 ago wenzelm tuned sort_ord: pointer_eq;
2005-06-29 ago wenzelm removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
2005-06-29 ago wenzelm eliminated separate syn type -- advanced trfuns already part of Syntax.syntax;
2005-06-29 ago wenzelm replaced Syntax.simple_pprint_typ by (Sign.pprint_typ ProtoPure.thy);
2005-06-29 ago wenzelm added implies_intr_hyps (from thm.ML);
2005-06-29 ago wenzelm added joinable;
2005-06-28 ago paulson stylistic improvements
2005-06-28 ago haftmann added project information in overview
2005-06-28 ago haftmann added project information in overview