Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
File.quote_sysify_path;
2004-06-21, by wenzelm
Merged in license change from Isabelle2004
2004-06-21, by kleing
got rid of Output.output for default print mode;
2004-06-20, by wenzelm
added checkTimer;
2004-06-20, by wenzelm
added accumulated timing;
2004-06-20, by wenzelm
added escape, export encode_raw, default mode now trivial, tuned;
2004-06-20, by wenzelm
use_output: Symbol.escape;
2004-06-20, by wenzelm
tuned pp;
2004-06-20, by wenzelm
avoid premature evaluation of syn_of (wastes time in conjunction with pp);
2004-06-20, by wenzelm
Symbol.encode_raw;
2004-06-20, by wenzelm
tuned;
2004-06-20, by wenzelm
improved comments -- required by 'isatool latex -o syms';
2004-06-18, by wenzelm
more generous treatment of packages in draft prints;
2004-06-18, by wenzelm
scalable string_of_tree; tuned;
2004-06-18, by wenzelm
tuned exists_string;
2004-06-18, by wenzelm
isatool_document: verbose option;
2004-06-18, by wenzelm
Add \usepackage{latexsym}
2004-06-18, by aspinall
new SAT solver interface
2004-06-17, by webertj
improved defcnf conversion
2004-06-17, by webertj
removal of magmas and semigroups
2004-06-17, by paulson
fixed 'requires' comments, which are needed for printing of drafts;
2004-06-17, by wenzelm
isub/isup quasi letter (again); tuned;
2004-06-17, by wenzelm
tuned;
2004-06-17, by wenzelm
tuned
2004-06-17, by schirmer
isatool_document: writeln output;
2004-06-16, by wenzelm
tuned document;
2004-06-16, by wenzelm
prevent looping of error messages involving malformed symbols;
2004-06-16, by wenzelm
tuned;
2004-06-16, by wenzelm
removed unused help function;
2004-06-16, by wenzelm
new fib example
2004-06-16, by paulson
removal of x-symbol syntax <Sigma> for dependent products
2004-06-16, by paulson
ISABELLE_TMP
2004-06-15, by wenzelm
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
removed norm_typ; improved output; refer to Pretty.pp;
2004-05-29, by wenzelm
moved read_int etc. to library.ML; added type 'arity';
2004-05-29, by wenzelm
improved output; refer to Pretty.pp;
2004-05-29, by wenzelm
Output.add_mode; Output.timing;
2004-05-29, by wenzelm
output channels and diagnostics moved to General/output.ML; added read_int etc. from term.ML; removed obsolete mtree; type rat uses exception RAT;
2004-05-29, by wenzelm
Output.timing;
2004-05-29, by wenzelm
improved output;
2004-05-29, by wenzelm
moved print_mode to General/output.ML; load General/pretty.ML early;
2004-05-29, by wenzelm
added Pure/General/output.ML;
2004-05-29, by wenzelm
avoid 'handle _' -- would cover Interrupt as well!!!
2004-05-29, by wenzelm
Sign.infer_types: Sign.pp;
2004-05-29, by wenzelm
Library.read_int;
2004-05-29, by wenzelm
Output.output;
2004-05-29, by wenzelm
'classrel': support multiple arguments;
2004-05-29, by wenzelm
* ML: all output via channels of writeln etc. passed through Output.output;
2004-05-29, by wenzelm
output channels;
2004-05-29, by wenzelm
added asm_lr_simplify/asm_lr_rewrite and adapted asm_full_simplify/asm_full_rewrite to match to corresponding simp_tacs
2004-05-28, by schirmer
new skolemize_tac and skolemize method
2004-05-28, by paulson
new theorem Collect_imp_eq
2004-05-28, by paulson
abstraction over functions is no default any more.
2004-05-26, by chaieb
adjusted for different signature of Type.typ_instance
2004-05-26, by webertj
mainly new/different datatype examples
2004-05-26, by webertj
documentation updated
2004-05-26, by webertj
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
2004-05-26, by webertj
new default parameters for refute
2004-05-26, by webertj
solver "auto" now issues a warning when it uses solver "enumerate"
2004-05-26, by webertj
Corrected printer bug for bounded quantifiers Q x<=y. P
2004-05-26, by nipkow
more group isomorphisms
2004-05-26, by paulson
added drop_take:thm
2004-05-24, by nipkow
- deleted unneeded function eta_long (now in Pure/pattern.ML
2004-05-21, by berghofe
Adapted to new syntax for case expressions.
2004-05-21, by berghofe
Added more flexible parse / print translations for case expressions.
2004-05-21, by berghofe
Modified functions pt_to_ast and ast_to_term to improve handling
2004-05-21, by berghofe
- exported result datatype
2004-05-21, by berghofe
updated;
2004-05-21, by wenzelm
Pure: clear separation of logical types and nonterminals;
2004-05-21, by wenzelm
adapted tsig/sg interface;
2004-05-21, by wenzelm
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
2004-05-21, by wenzelm
added fold, product; removed transitive_closure;
2004-05-21, by wenzelm
adapted names of some sort ops;
2004-05-21, by wenzelm
major cleanup of tsig datastructures and extend/merge operations; fixes old bugs in classes/arities code; proper treatment of nonterminals and syntax-only types;
2004-05-21, by wenzelm
Type.strip_sorts;
2004-05-21, by wenzelm
incorporate type inference interface from type.ML;
2004-05-21, by wenzelm
adapted tsig interface;
2004-05-21, by wenzelm
moved some sort ops to sorts.ML; added string_of_vname (from Syntax module);
2004-05-21, by wenzelm
test_classrel/arity improve error reporting; tuned;
2004-05-21, by wenzelm
xxx_typ_raw replace xxx_typ_no_norm forms; prevent duplicate consts declarations in merge; misc cleanup;
2004-05-21, by wenzelm
string_of_vname moved to term.ML;
2004-05-21, by wenzelm
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
2004-05-21, by wenzelm
type.ML now before Syntax module;
2004-05-21, by wenzelm
xxx_typ_raw replace xxx_typ_no_norm forms;
2004-05-21, by wenzelm
'classrel' now allows multiple arguments;
2004-05-21, by wenzelm
Sign.certify_tyname;
2004-05-21, by wenzelm
TypeInfer.paramify_dummies, TypeInfer.param;
2004-05-21, by wenzelm
Args.local_typ_raw;
2004-05-21, by wenzelm
output_tym: removed duplicate clauses;
2004-05-21, by wenzelm
Graph.minimals;
2004-05-21, by wenzelm
adapted syntax to cope with lack of non-logical types;
2004-05-21, by wenzelm
Type.typ_instance;
2004-05-21, by wenzelm
load ML files only once;
2004-05-21, by wenzelm
removed duplicate thms;
2004-05-21, by wenzelm
Sign.typ_instance;
2004-05-21, by wenzelm
tuned message;
2004-05-21, by wenzelm
tuned document;
2004-05-21, by wenzelm
use plain SOME;
2004-05-21, by wenzelm
proper use of 'syntax';
2004-05-21, by wenzelm
auto update
2004-05-19, by paulson
has_consts now handles the @-operator
2004-05-19, by paulson
new bij_betw operator
2004-05-19, by paulson
more results about isomorphisms
2004-05-19, by paulson
conversion of Hilbert_Choice to Isar script
2004-05-19, by paulson
the function list1 has been exported.
2004-05-19, by chaieb
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
2004-05-19, by chaieb
tactic call changed from TRYALL arith_tac to TRYALL simple_arith_tac preventing a call to presburger.
2004-05-19, by chaieb
modified abel_cancel.ML for polymorphic types
2004-05-18, by obua
simplification for abelian groups
2004-05-18, by obua
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
2004-05-18, by obua
Comments fixed
2004-05-17, by webertj
lemma disjoint_int_union removed - too special
2004-05-17, by mehta
Change of theory hierarchy: Group is now based in Lattice.
2004-05-14, by ballarin
tidied
2004-05-14, by paulson
new atomize theorem
2004-05-14, by paulson
removed a premise of card_inj_on_le
2004-05-14, by paulson
removal of locale coset
2004-05-14, by paulson
deleted redundant proof lines
2004-05-14, by paulson
new lemmas
2004-05-14, by paulson
clauses for ordinary resolution
2004-05-14, by paulson
conversion of theorems to atomic form
2004-05-14, by paulson
less
more
|
(0)
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
+30000
tip