isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -10000 -3000 -1000 -120 +120 +1000 +3000 +10000 +30000 tip

Moved eq_type from envir.ML to type.ML
2005-07-01, by berghofe
Implemented modular code generation.
2005-07-01, by berghofe
Simplified proof (thanks to strengthened ball_cong).
2005-07-01, by berghofe
Proof of wx_ex_prop must now use old bex_cong to prevent simplifier from looping.
2005-07-01, by berghofe
Adapted to new interface of RecfunCodegen.add.
2005-07-01, by berghofe
Adapted to modular code generation.
2005-07-01, by berghofe
Corrected implementation of arbitrary on cname.
2005-07-01, by berghofe
Added BasisLibrary prefix to List.concat to avoid problems with
2005-07-01, by berghofe
Moved code generator setup from NatBin to IntDef.
2005-07-01, by berghofe
Simplified some proofs (thanks to strong_setsum_cong).
2005-07-01, by berghofe
Removed setsubgoaler hack (thanks to strong_setsum_cong).
2005-07-01, by berghofe
Removed setsubgoaler hack (thanks to strengthened finsum_cong).
2005-07-01, by berghofe
Removed setsubgoaler hack.
2005-07-01, by berghofe
Tuned finsum_cong to allow that premises are simplified more eagerly.
2005-07-01, by berghofe
Added strong_ball_cong and strong_bex_cong (these are now the standard
2005-07-01, by berghofe
Moved some code lemmas from Main to Nat.
2005-07-01, by berghofe
Adapted to new interface of code generator.
2005-07-01, by berghofe
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
2005-07-01, by berghofe
Added strong_setsum_cong and strong_setprod_cong.
2005-07-01, by berghofe
defaultsort pcpo
2005-07-01, by huffman
added theorem lift_definedE; moved cont_if to Cont.thy
2005-07-01, by huffman
added tactic cont_tac
2005-07-01, by huffman
remove uses of sign_of
2005-07-01, by huffman
cleaned up
2005-07-01, by huffman
cleaned up
2005-07-01, by huffman
renamed flatdom2monofun to flatdom_strict2mono
2005-07-01, by huffman
cleaned up; reorganized and added section headings
2005-07-01, by huffman
cleaned up; added adm_less to adm_lemmas; added subsection headings
2005-07-01, by huffman
revert to 1.27 due to obscure performance issues (!??);
2005-06-30, by wenzelm
replace filter2 with List.partition
2005-06-30, by huffman
Proper treatment of beta-redexes in witness theorems.
2005-06-30, by ballarin
minor corrections
2005-06-30, by haftmann
test sml-dev on mac as well
2005-06-30, by kleing
use only 1 CPU on MacOS 10.4.1
2005-06-30, by kleing
use kleing@cse instead of kleing@in.tum.de
2005-06-30, by kleing
use global settings for isatest-doc
2005-06-30, by kleing
export no_type_brackets;
2005-06-29, by wenzelm
proper treatment of advanced trfuns: pass thy argument;
2005-06-29, by wenzelm
transform_failure in translation functions: TRANSLATION_FAIL;
2005-06-29, by wenzelm
proper treatment of advanced trfuns: pass thy argument;
2005-06-29, by wenzelm
accomodate advanced trfuns;
2005-06-29, by wenzelm
removed obsolete (un)fold_ast2;
2005-06-29, by wenzelm
Drule.implies_intr_hyps;
2005-06-29, by wenzelm
added print': print depending on print_mode;
2005-06-29, by wenzelm
no Syntax.internal on thesis;
2005-06-29, by wenzelm
added print_mode three_buffersN and corresponding cond_print;
2005-06-29, by wenzelm
cond_print for end-of-proof and calculational commands;
2005-06-29, by wenzelm
added eq;
2005-06-29, by wenzelm
pass thy as explicit argument (the old ref was not safe
2005-06-29, by wenzelm
more efficient treatment of shyps and hyps (use ordered lists);
2005-06-29, by wenzelm
Syntax.read thy;
2005-06-29, by wenzelm
tuned sort_ord: pointer_eq;
2005-06-29, by wenzelm
removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
2005-06-29, by wenzelm
eliminated separate syn type -- advanced trfuns already part of Syntax.syntax;
2005-06-29, by wenzelm
replaced Syntax.simple_pprint_typ by (Sign.pprint_typ ProtoPure.thy);
2005-06-29, by wenzelm
added implies_intr_hyps (from thm.ML);
2005-06-29, by wenzelm
added joinable;
2005-06-29, by wenzelm
stylistic improvements
2005-06-28, by paulson
added project information in overview
2005-06-28, by haftmann
added project information in overview
2005-06-28, by haftmann
more sophisticated pypager
2005-06-28, by haftmann
first-order check now allows quantifiers
2005-06-28, by paulson
stricter first-order check for meson
2005-06-28, by paulson
Constant "If" is now local
2005-06-28, by paulson
more sophisticated pypager
2005-06-28, by haftmann
replacing zabs_def by abs_if
2005-06-28, by paulson
introduced a notion of mirrors
2005-06-28, by haftmann
some minor improvements
2005-06-28, by haftmann
some minor improvements
2005-06-28, by haftmann
some minor improvements
2005-06-28, by haftmann
some minor improvements
2005-06-28, by haftmann
some minor improvements
2005-06-28, by haftmann
some minor improvements
2005-06-28, by haftmann
some minor improvements
2005-06-28, by haftmann
some minor improvements
2005-06-28, by haftmann
some minor improvements
2005-06-28, by haftmann
some minor improvements
2005-06-28, by haftmann
corrected comment
2005-06-28, by haftmann
some corrections
2005-06-28, by haftmann
export get_calculation;
2005-06-26, by wenzelm
Added term_lpo
2005-06-25, by nipkow
cancels completely within terms as well now.
2005-06-25, by nipkow
Changes due to new abel_cancel.ML
2005-06-25, by nipkow
use both processors on macbroy5
2005-06-25, by kleing
switch mac test to macbroy5
2005-06-25, by kleing
cleaned up
2005-06-25, by huffman
cleaned up proof of contlub_abstraction
2005-06-25, by huffman
meson method taking an argument list
2005-06-24, by paulson
deleted a redundant "use" line
2005-06-24, by paulson
tidying
2005-06-24, by paulson
stylistic tweaks concerning Find
2005-06-24, by paulson
shortened time out by 3h (gives up at 12:00h now).
2005-06-24, by kleing
made su[bp]/isu[bp] behave the same as their bsu[bp]..esu[bp] counterparts,
2005-06-24, by kleing
needed for Isabelle independent build
2005-06-24, by kleing
added theorems fix_strict, fix_defined, fix_id, fix_const
2005-06-23, by huffman
add binder syntax for flift1
2005-06-23, by huffman
add new file to test fixrec package
2005-06-23, by huffman
add csplit3, ssplit3, fup3 as simp rules
2005-06-23, by huffman
New features:
2005-06-23, by huffman
added match functions for spair, sinl, sinr
2005-06-23, by huffman
fixed \<Prod> syntax
2005-06-23, by nipkow
new
2005-06-23, by nipkow
Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
2005-06-22, by quigley
* Pure: the Isar proof context type is already defined early in Pure
2005-06-22, by wenzelm
added find2
2005-06-22, by nipkow
*** empty log message ***
2005-06-22, by nipkow
tunes Find
2005-06-22, by nipkow
added Rules/find2
2005-06-22, by nipkow
tuned pointer_eq;
2005-06-22, by wenzelm
renamed data kind;
2005-06-22, by wenzelm
removed proof data (see Pure/context.ML);
2005-06-22, by wenzelm
added depth_of;
2005-06-22, by wenzelm
removed obsolete object.ML (see Pure/library.ML);
2005-06-22, by wenzelm
export sort_ord;
2005-06-22, by wenzelm
renamed init to init_data;
2005-06-22, by wenzelm
added structure Object (from Pure/General/object.ML);
2005-06-22, by wenzelm
tuned;
2005-06-22, by wenzelm
begin_thy: merge maximal imports;
2005-06-22, by wenzelm
removed Pure/Isar/proof_data.ML, Pure/General/object.ML;
2005-06-22, by wenzelm
improved proof;
2005-06-22, by wenzelm