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

path instead of string;
2004-06-15, by wenzelm
added path;
2004-06-15, by wenzelm
tuned lexical syntax;
2004-06-15, by wenzelm
num tokens;
2004-06-15, by wenzelm
fixed bad link
2004-06-15, by paulson
slight speed improvement
2004-06-15, by paulson
strengthened some theorems
2004-06-15, by paulson
Jerusat settings added
2004-06-15, by webertj
entries for ZChaff and BerkMin added/modified
2004-06-15, by webertj
Oracle corrected
2004-06-14, by chaieb
Further development of matrix theory
2004-06-14, by obua
faster defcnf conversion
2004-06-13, by webertj
updated;
2004-06-13, by wenzelm
updated;
2004-06-13, by wenzelm
tuned;
2004-06-13, by wenzelm
tuned Present.drafts;
2004-06-13, by wenzelm
added display_drafts and print_drafts commands;
2004-06-13, by wenzelm
added PRINT_COMMAND setting
2004-06-13, by wenzelm
added isatool display and isatool print;
2004-06-13, by wenzelm
print document
2004-06-13, by wenzelm
display document (in DVI format)
2004-06-13, by wenzelm
root for draft documents;
2004-06-12, by wenzelm
Library.translate_string;
2004-06-12, by wenzelm
added trace (inefficient for very long input);
2004-06-12, by wenzelm
added translate_string;
2004-06-12, by wenzelm
added read (provides transition names and sources);
2004-06-12, by wenzelm
added output_known_symbols; tuned;
2004-06-12, by wenzelm
added name_of, source_of, source;
2004-06-12, by wenzelm
added Present.drafts;
2004-06-12, by wenzelm
added option 'isatool latex -o syms';
2004-06-12, by wenzelm
An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.
2004-06-12, by chaieb
tuned;
2004-06-10, by wenzelm
improved RemoteFile;
2004-06-10, by wenzelm
tuned;
2004-06-10, by wenzelm
Removed this: not really ready yet.
2004-06-10, by aspinall
Interface configuration for Isar
2004-06-10, by aspinall
Sign.is_logtype;
2004-06-09, by wenzelm
prs: Output.output;
2004-06-09, by wenzelm
added split_ext; removed drop_ext;
2004-06-09, by wenzelm
tuned comment;
2004-06-09, by wenzelm
Scan.this_string;
2004-06-09, by wenzelm
tuned representation; added RemoteFile;
2004-06-09, by wenzelm
tuned;
2004-06-09, by wenzelm
added this_string;
2004-06-09, by wenzelm
tuned messages;
2004-06-09, by wenzelm
added is_logtype (replaces logtypes field of syntax); tuned merge;
2004-06-09, by wenzelm
removed separate logtypes field of syntax; removed test_read, simple_str_of_sort, simple_string_of_typ; provide default_mode;
2004-06-09, by wenzelm
removed separate logtypes field of syntax;
2004-06-09, by wenzelm
Path.split_ext; more robust inform_file_processed;
2004-06-09, by wenzelm
Sign.is_logtype;
2004-06-09, by wenzelm
Syntax.default_mode;
2004-06-09, by wenzelm
added option 'locale=NAME';
2004-06-09, by wenzelm
Url.File;
2004-06-09, by wenzelm
* Document preparation: antiquotations provide option 'locale=NAME';
2004-06-09, by wenzelm
tuned comment;
2004-06-09, by wenzelm
updated/tuned identifier syntax;
2004-06-09, by wenzelm
updated notes on sub-/superscripts;
2004-06-09, by wenzelm
removed Syntax.test_read;
2004-06-09, by wenzelm
added a lemma lfp_ordinal_induct
2004-06-09, by nipkow
fixed the groupI ambiguity
2004-06-09, by paulson
fixed the skolemize method
2004-06-09, by paulson
moved some cardinality results into main HOL
2004-06-09, by paulson
add_dummies no longer uses transform_error but handles specific
2004-06-08, by berghofe
Added exception Datatype_Empty.
2004-06-08, by berghofe
mk_id is now also applied to identifiers in test_term.
2004-06-08, by berghofe
Groups, Rings and supporting lemmas in ZF
2004-06-08, by paulson
Groups, Rings and supporting lemmas
2004-06-08, by paulson
Groups, Rings and supporting lemmas
2004-06-08, by paulson
avoid Args.list (lost update?);
2004-06-06, by wenzelm
added has_mode; handle_error: output raw;
2004-06-06, by wenzelm
Symbol.output;
2004-06-06, by wenzelm
no token translation / setup for Latex;
2004-06-06, by wenzelm
HOL: symbolic syntax of Eps;
2004-06-06, by wenzelm
More readable code.
2004-06-05, by chaieb
pretty_thm/goals_aux, pretty_flexpair: pp;
2004-06-05, by wenzelm
avoid implicit arguments via refs;
2004-06-05, by wenzelm
Symbol.decode;
2004-06-05, by wenzelm
added datatype sym, val decode: symbol -> sym;
2004-06-05, by wenzelm
improved symbolic syntax of Eps: \<some> for mode "epsilon";
2004-06-05, by wenzelm
removed mlworks and smlnj-0.93 (obsolete);
2004-06-05, by wenzelm
tuned comments;
2004-06-05, by wenzelm
moved exception handling back to library.ML;
2004-06-05, by wenzelm
tuned exeption handling (capture/release);
2004-06-05, by wenzelm
removed Pure/ML-Systems/mlworks.ML Pure/ML-Systems/polyml-3.x.ML Pure/ML-Systems/smlnj-0.93.ML; added ML-Systems/polyml-time-limit.ML;
2004-06-05, by wenzelm
obsolete;
2004-06-05, by wenzelm
Tuned parse_att.
2004-06-04, by berghofe
new rules for simplifying quantifiers with Sigma
2004-06-02, by paulson
Add alternative syntax for attributes
2004-06-01, by aspinall
Add panic function which exits Isabelle immediately.
2004-06-01, by aspinall
Removed ~10000 hack in function idx that can lead to inconsistencies
2004-06-01, by berghofe
Adapted to new name mangling function in code generator.
2004-06-01, by berghofe
Adapted to new name mangling function.
2004-06-01, by berghofe
Improved name mangling function.
2004-06-01, by berghofe
proper use of 'nonterminals';
2004-06-01, by wenzelm
proper treatment of logical types within syntax;
2004-06-01, by wenzelm
removed obsolete sort 'logic' and '=?=' syntax;
2004-06-01, by wenzelm
removed obsolete sort 'logic';
2004-06-01, by wenzelm
more on bij_betw
2004-06-01, by paulson
tidied
2004-06-01, by paulson
TimeLimit structure added (no proper implementation yet)
2004-06-01, by webertj
including polyml-time-limit.ML
2004-06-01, by webertj
SML/NJs TimeLimit structure ported to Poly/ML
2004-06-01, by webertj
oops -- no Output.out here;
2004-05-31, by wenzelm
updated;
2004-05-29, by wenzelm
\<^bsub>/\<^esub> syntax: unbreakable block;
2004-05-29, by wenzelm
\<^bsub>/\<^esub> syntax: unbreakable block;
2004-05-29, by wenzelm
Scan.this; tuned;
2004-05-29, by wenzelm
do *not* export list/list1 -- commas considered special in arg syntax;
2004-05-29, by wenzelm
target 'generate';
2004-05-29, by wenzelm
avoid Args.list;
2004-05-29, by wenzelm
handle raw symbols; Output.add_mode;
2004-05-29, by wenzelm
handle raw symbols; Output.add_mode; more robust handling of sub/superscript;
2004-05-29, by wenzelm
tuned _dummy_ofsort syntax;
2004-05-29, by wenzelm
added pp_show_brackets; support unbreakable blocks;
2004-05-29, by wenzelm
transform_error;
2004-05-29, by wenzelm
Library.read_int; Output.output;
2004-05-29, by wenzelm
improved support for raw symbols;
2004-05-29, by wenzelm
Output.error;
2004-05-29, by wenzelm
pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
2004-05-29, by wenzelm
added Pure/General/output.ML; load Pure/General/pretty.ML early in Pure/ROOT.ML;
2004-05-29, by wenzelm