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

build Isabelle process wrapper;
2008-01-06, by wenzelm
* Rudimentary Isabelle plugin for jEdit;
2008-01-06, by wenzelm
added plugin installation;
2008-01-06, by wenzelm
tuned;
2008-01-06, by wenzelm
purge build directory;
2008-01-06, by wenzelm
basic setup for Isabelle/jEdit plugin;
2008-01-06, by wenzelm
added interface for command-line option;
2008-01-06, by wenzelm
removed obsolete prompt and channel markups;
2008-01-06, by wenzelm
replaced prompt markup by prompt channel setup;
2008-01-06, by wenzelm
removed obsolete prompt markup;
2008-01-06, by wenzelm
removed unused of_stream;
2008-01-06, by wenzelm
added explicit prompt channel (prompt_fn/prompt);
2008-01-06, by wenzelm
removed obsolete prompt and channel markups;
2008-01-06, by wenzelm
Tuned relevant premises selection
2008-01-05, by chaieb
tuned comments;
2008-01-05, by wenzelm
added symbol output mode, with XML escapes;
2008-01-05, by wenzelm
export session id;
2008-01-05, by wenzelm
secure_main: removed separate welcome;
2008-01-05, by wenzelm
removed unused text_charref, cdata;
2008-01-05, by wenzelm
added INIT message, with pid and session property;
2008-01-05, by wenzelm
more instantiation
2008-01-05, by haftmann
adhering to instantiation policy
2008-01-05, by haftmann
cleaned up some proofs
2008-01-04, by huffman
simplified some proofs
2008-01-04, by huffman
partially adapted to new inversion rules
2008-01-04, by urbanc
adapted to new inversion rules
2008-01-04, by urbanc
fixed typo
2008-01-04, by haftmann
improved warning
2008-01-04, by haftmann
add new is_ub lemmas; clean up directed_finite proofs
2008-01-04, by huffman
new instance proofs for classes finite_po, chfin, flat
2008-01-04, by huffman
new lemma flat_less_iff
2008-01-03, by huffman
generalized chfindom_monofun2cont
2008-01-03, by huffman
Implemented proof of strong case analysis rule.
2008-01-03, by berghofe
Added function fresh_const.
2008-01-03, by berghofe
Added function partition_rules'.
2008-01-03, by berghofe
another attempt to disable documents;
2008-01-03, by wenzelm
simplified position_props, always include line/file fields;
2008-01-03, by wenzelm
replaced thread_properties by simplified version in position.ML;
2008-01-03, by wenzelm
nested_command: simplified properties vs. position -- the latter also includes id now;
2008-01-03, by wenzelm
type T: based on properties, added id field;
2008-01-03, by wenzelm
moved id to position properties;
2008-01-03, by wenzelm
instance unit :: finite_po
2008-01-03, by huffman
new axclass finite_po < finite, po
2008-01-03, by huffman
add lub_maximal lemmas;
2008-01-03, by huffman
added class Property: basic Isabelle properties;
2008-01-03, by wenzelm
tuned relevance test for presburger
2008-01-03, by chaieb
output message properties: id or position;
2008-01-03, by wenzelm
toplevel print_exn: proper setmp_thread_properties;
2008-01-03, by wenzelm
added id property;
2008-01-03, by wenzelm
Result: added props field;
2008-01-03, by wenzelm
remove legacy ML bindings
2008-01-03, by huffman
new-style theorem references
2008-01-03, by huffman
fix theorem references
2008-01-03, by huffman
generalized and simplified proof of adm_Finite
2008-01-03, by huffman
new lemma adm_upward
2008-01-03, by huffman
Tuned (type information in Lemmas)
2008-01-03, by chaieb
Changed order of tactics in presburger --- thinning before case splits
2008-01-03, by chaieb
maintain thread transition properties;
2008-01-03, by wenzelm
setmp_thread_data;
2008-01-03, by wenzelm
added setmp_thread_data;
2008-01-03, by wenzelm
type transition: added properties field;
2008-01-02, by wenzelm
added properties;
2008-01-02, by wenzelm
Isabelle.command: IsarCmd.nested_command (with properties);
2008-01-02, by wenzelm
added nested_command (with explicit position argument via properties);
2008-01-02, by wenzelm
of_properties: return filtered result;
2008-01-02, by wenzelm
added method encodeProperties;
2008-01-02, by wenzelm
setting -H 2000 and no documents for higher performance;
2008-01-02, by wenzelm
add dcpo instance proof
2008-01-02, by huffman
declare upE as cases rule; add new rule up_induct
2008-01-02, by huffman
update sq_ord/po instance proofs
2008-01-02, by huffman
move lemmas from Cont.thy to Ffun.thy;
2008-01-02, by huffman
remove not_up_less_UU [simp]
2008-01-02, by huffman
update instance proofs for sq_ord, po; new instance proofs for dcpo
2008-01-02, by huffman
add lemma ub2ub_monofun'
2008-01-02, by huffman
added dcpo instance proofs
2008-01-02, by huffman
new class dcpo; added dcpo versions of some lemmas
2008-01-02, by huffman
added new lemmas
2008-01-02, by huffman
add lemma dir2dir_monofun
2008-01-02, by huffman
tuned;
2008-01-02, by wenzelm
new is_ub lemmas; new lub syntax for set image
2008-01-02, by huffman
Multithreading.max_threads := 0 refers to number of cores of underlying machine;
2008-01-02, by wenzelm
added Multithreading.max_threads_value, which maps a value of 0 to number of CPUs;
2008-01-02, by wenzelm
added usedir -M max (alias for -M 0);
2008-01-02, by wenzelm
new section for directed sets
2008-01-02, by huffman
split of class uminus
2008-01-02, by haftmann
empty dictionaries for OCaml
2008-01-02, by haftmann
clarified policy
2008-01-02, by haftmann
tuned
2008-01-02, by haftmann
some more antiquotations
2008-01-02, by haftmann
index now a copy of nat rather than int
2008-01-02, by haftmann
absolute import
2008-01-02, by haftmann
some more primrec
2008-01-02, by haftmann
removed some legacy instantiations
2008-01-02, by haftmann
improved evaluation mechanism
2008-01-02, by haftmann
splitted class uminus from class minus
2008-01-02, by haftmann
testing for empty sort
2008-01-02, by paulson
new metis proofs
2008-01-02, by paulson
renamed foldM to fold_mset on general request
2008-01-02, by kleing
update instance proofs to new style
2008-01-02, by huffman
declare sprodE as cases rule; new induction rule sprod_induct
2008-01-01, by huffman
add induction rule ssum_induct
2008-01-01, by huffman
eval_wrapper: CRITICAL;
2008-01-01, by wenzelm
try_ml_file: setmp explicit theory context, prevents race condition wrt. concurrent ML_Context.set_context;
2008-01-01, by wenzelm
tuned spaces;
2008-01-01, by wenzelm
removed separate exists/forall code;
2008-01-01, by wenzelm
tuned proofs and comments
2008-01-01, by urbanc
removed obsolete banner;
2007-12-31, by wenzelm
tuned;
2007-12-30, by wenzelm
added PROMPT message;
2007-12-30, by wenzelm
added isSystem;
2007-12-30, by wenzelm
simple make script;
2007-12-30, by wenzelm
tuned comments (javadoc);
2007-12-29, by wenzelm
use polyml-cvs, the 5.2 development branch;
2007-12-27, by wenzelm
tuned RandomWord interface;
2007-12-22, by wenzelm
added int/real/list operations;
2007-12-22, by wenzelm
use random_word.ML earlier;
2007-12-22, by wenzelm
changed type definition to make Iwhen and reasoning about chains unnecessary;
2007-12-21, by huffman
Fixed eta constraction issue in compose_witness
2007-12-21, by ballarin
included meson/metis tests in simultaneous use_thys;
2007-12-20, by wenzelm
``print mode'' is now a thread-local value derived from a global template;
2007-12-20, by wenzelm