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.
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
New simp rules added:
2004-05-13, by mehta
simpilified and strengthened proofs
2004-05-12, by paulson
fixed latex problems
2004-05-12, by nipkow
renamed `> to o_m
2004-05-12, by nipkow
changes made due to new Ring_and_Field theory
2004-05-11, by obua
Eta-expanded function scan_comment to make SmlNJ happy.
2004-05-11, by berghofe
broken no longer includes TTP, and other minor changes
2004-05-11, by paulson
removal of prime characters
2004-05-11, by paulson
package needed for superscripts
2004-05-11, by paulson
conversion to clauses for ordinary resolution rather than ME
2004-05-11, by paulson
auto update
2004-05-11, by paulson
Pure: nested comments in inner syntax;
2004-05-10, by wenzelm
support nested comments;
2004-05-10, by wenzelm
changed Symbol.beginning;
2004-05-10, by wenzelm
tuned;
2004-05-10, by wenzelm
Source.of_list: no buffer limitation (now pointless due to tail-recursive Scan.repeat);
2004-05-10, by wenzelm
added Scan.list;
2004-05-10, by wenzelm
ProofGeneral.process_pgip command;
2004-05-10, by wenzelm
preparation for integration with new Ring_and_Field.thy
2004-05-10, by obua
moved first lemma in LongDiv.ML to LongDiv.thy
2004-05-10, by obua
replaced apply-style proof for instance Multiset :: plus_ac0 by recommended Isar proof style
2004-05-09, by obua
removed Aux.thy;
2004-05-09, by bauerg
cleanup up read functions, include liberal versions;
2004-05-07, by wenzelm
be liberal about constant names;
2004-05-07, by wenzelm
tuned;
2004-05-07, by wenzelm
tuned notation;
2004-05-07, by wenzelm
tuned document;
2004-05-07, by wenzelm
*** empty log message ***
2004-05-07, by bauerg
Add FIXME note re FAIL (is it fixed yet?)
2004-05-07, by aspinall
Add cdata output. Add tabs in whitespace. Write two strings instead of Library.quote.
2004-05-07, by aspinall
Add -X option to trigger PGIP interaction mode.
2004-05-07, by aspinall
*** empty log message ***
2004-05-07, by bauerg
replaced Aux.thy by RealLemmas.thy
2004-05-07, by bauerg
tuned HOL/record package; enabled record_upd_simproc by default.
2004-05-06, by schirmer
improved block sup/sub;
2004-05-06, by wenzelm
show_structs option;
2004-05-06, by wenzelm
tuned document;
2004-05-06, by wenzelm
tidied
2004-05-06, by paulson
auto update
2004-05-06, by paulson
redundant clause removed
2004-05-04, by webertj
solved sml-nj compatibility problem
2004-05-04, by schirmer
tuned;
2004-05-04, by schirmer
reimplementation of HOL records; only one type is created for
2004-05-03, by schirmer
tuned;
2004-05-01, by wenzelm
improvd indexed syntax and implicit structures; tuned renaming of symbolic identifiers
2004-05-01, by wenzelm
less
more
|
(0)
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
+30000
tip