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

removed timers;
2005-07-06, by wenzelm
debug: exception_trace;
2005-07-06, by wenzelm
finish: Output.accumulated_time;
2005-07-06, by wenzelm
dest_parsers: sort result;
2005-07-06, by wenzelm
added time_accumulator and accumulated_time supercede
2005-07-06, by wenzelm
added full_prop_of: includes tpairs;
2005-07-06, by wenzelm
tuned eq_ix;
2005-07-06, by wenzelm
Context.check_thy;
2005-07-06, by wenzelm
tuned forall_elim_var(s): avoid expensive Term.add_vars;
2005-07-06, by wenzelm
tuned;
2005-07-06, by wenzelm
Thm.full_prop_of;
2005-07-06, by wenzelm
check_thy: less invocations, less verbose;
2005-07-06, by wenzelm
* Pure: Output.time_accumulator;
2005-07-06, by wenzelm
isatool fixheaders;
2005-07-06, by wenzelm
tuned msg;
2005-07-06, by wenzelm
ThyInfo.time_use root;
2005-07-06, by wenzelm
added output_buffer;
2005-07-06, by wenzelm
added write_list, append_list;
2005-07-06, by wenzelm
tuned write: use File.write_list;
2005-07-06, by wenzelm
tuned maxidx;
2005-07-06, by wenzelm
tuned maxidx_of_typ/typs/term;
2005-07-06, by wenzelm
multiple flags: prefer later ones;
2005-07-06, by wenzelm
use Symtab.table instead of ordered lists;
2005-07-06, by wenzelm
added adhoc string_of_term from Pure/term.ML;
2005-07-06, by wenzelm
removed term_lpo (now in Pure/term.ML);
2005-07-06, by wenzelm
tuned;
2005-07-06, by wenzelm
tuned;
2005-07-06, by wenzelm
changed file permissions;
2005-07-06, by wenzelm
changing file permissions ...
2005-07-06, by wenzelm
add keywords cpodef, pcpodef (for HOLCF)
2005-07-06, by huffman
renamed to Pcpodef.thy
2005-07-06, by huffman
use new pcpodef package
2005-07-06, by huffman
add pcpodef files
2005-07-06, by huffman
renamed from TypedefPcpo.thy;
2005-07-06, by huffman
new type definition package for HOLCF
2005-07-06, by huffman
simplified definitions of flift1, flift2, liftpair;
2005-07-05, by huffman
tuned K;
2005-07-05, by wenzelm
fixed regexp grouping;
2005-07-05, by wenzelm
List.app;
2005-07-05, by wenzelm
added combinatros '||>' and '||>>' and fold_map fitting nicely to ST combinator '|->'
2005-07-05, by haftmann
tuned;
2005-07-05, by wenzelm
* Pure: structure OrdList (cf. Pure/General/ord_list.ML);
2005-07-05, by wenzelm
added ST combinator '|->'
2005-07-05, by haftmann
Symtab: use fast_string_ord instead of string_ord -- affects order of Symtab.dest etc.;
2005-07-05, by wenzelm
tuned;
2005-07-05, by wenzelm
made smlnj happy;
2005-07-04, by wenzelm
methods: added simp_flags argument, added "depth_limit" flag;
2005-07-04, by wenzelm
added transform_exceptions: bool ref;
2005-07-04, by wenzelm
tuned;
2005-07-04, by wenzelm
dummy exception_trace;
2005-07-04, by wenzelm
tuned union: avoid garbage in trivial case;
2005-07-04, by wenzelm
dest_ctyp: raise exception for non-constructor;
2005-07-04, by wenzelm
added fast_indexname_ord, fast_term_ord;
2005-07-04, by wenzelm
use fast_string_ord;
2005-07-04, by wenzelm
added fast_string_ord;
2005-07-04, by wenzelm
Streamlined the signal handler in watcher.ML
2005-07-04, by quigley
unified main and dist
2005-07-04, by haftmann
started unifying main and dist
2005-07-04, by haftmann
(intermediate commit)
2005-07-04, by haftmann
Simple report generator for Poly/ML profiling output.
2005-07-02, by wenzelm
tuned;
2005-07-01, by wenzelm
ambig msg: warning again;
2005-07-01, by wenzelm
avoid polyeq;
2005-07-01, by wenzelm
tuned term_ord: less garbage;
2005-07-01, by wenzelm
cterm_aconv: avoid rep_cterm;
2005-07-01, by wenzelm
decomp_simp: compare terms, not cterms;
2005-07-01, by wenzelm
back to 1.28;
2005-07-01, by wenzelm
prime is a predicate now.
2005-07-01, by nipkow
* Isar profiling: new reference Toplevel.profiling (default 0);
2005-07-01, by wenzelm
use tracing for potentially voluminous ambiguity output;
2005-07-01, by wenzelm
added profiler interface (dummy);
2005-07-01, by wenzelm
added profiler interface, keep 'profiling' of PolyML structure;
2005-07-01, by wenzelm
added profile flag;
2005-07-01, by wenzelm
low-level tuning of map, fold;
2005-07-01, by wenzelm
ctyp: added 'sorts' field;
2005-07-01, by wenzelm
added all_sorts_nonempty;
2005-07-01, by wenzelm
low-level tuning of fold, fold_rev, foldl_map;
2005-07-01, by wenzelm
isatool install: removed KDE option;
2005-07-01, by wenzelm
Fixed bug: lookup' must use = instead of eq_type to compare types of
2005-07-01, by berghofe
Changed interface of Envir.lookup'
2005-07-01, by berghofe
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