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

Replaced iteration combinator by recursion combinator.
2006-03-23, by berghofe
detection of definitions of relevant constants
2006-03-23, by paulson
Only display atpset theorems if Output.show_debug_msgs is true.
2006-03-23, by mengj
added the first two simple proofs of the recursion
2006-03-22, by urbanc
comment fixed
2006-03-22, by webertj
Introduction of "whitelist": theorems forced past the relevance filter
2006-03-22, by paulson
Slight simplification of proofs
2006-03-22, by paulson
Removal of obsolete strategies. Initial support for locales: Frees and Consts
2006-03-22, by paulson
comment for conjI added
2006-03-22, by webertj
translations -> abbreviations (a cool feature)
2006-03-22, by nipkow
fixed example;
2006-03-21, by wenzelm
mark_boundT: produce well-typed term;
2006-03-21, by wenzelm
subtract (op =);
2006-03-21, by wenzelm
avoid polymorphic equality;
2006-03-21, by wenzelm
avoid polymorphic equality;
2006-03-21, by wenzelm
moved gen_eq_set to library.ML;
2006-03-21, by wenzelm
added ~$$ (negative literal);
2006-03-21, by wenzelm
avoid polymorphic equality;
2006-03-21, by wenzelm
remove (op =);
2006-03-21, by wenzelm
gen_eq_set, remove (op =);
2006-03-21, by wenzelm
abbreviation upto, length;
2006-03-21, by wenzelm
added subtract;
2006-03-21, by wenzelm
subtract (op =);
2006-03-21, by wenzelm
remove (op =);
2006-03-21, by wenzelm
Now SML/NJ-friendly (IntInf)
2006-03-21, by paulson
Removal of unnecessary simprules: simproc cancel_numerals now works without
2006-03-21, by paulson
interpret: Proof.assert_forward_or_chain;
2006-03-20, by wenzelm
subsetI is often necessary
2006-03-20, by paulson
Now the setup for cancel_numerals accepts mixed Sucs/+ where the Sucs no longer
2006-03-20, by paulson
Tuned signature of Locale.add_locale(_i).
2006-03-20, by ballarin
simplified mg_domain (use Sign.classes/arities_of);
2006-03-18, by wenzelm
made $$ and "this" monomorphic (string);
2006-03-18, by wenzelm
tuned;
2006-03-18, by wenzelm
export arities_of instead of classes_arities_of;
2006-03-18, by wenzelm
updated;
2006-03-18, by wenzelm
renamed const less to lt;
2006-03-18, by wenzelm
renamed constant less in lattice
2006-03-18, by haftmann
fixed problem with proof reconstruction by adding add_Suc to arith-simpset.
2006-03-17, by nipkow
added parser locale_expr_unless
2006-03-17, by schirmer
fixed clsvar bug
2006-03-17, by haftmann
add_locale(_i) returns internal locale name.
2006-03-17, by ballarin
added example for operational classes and code generator
2006-03-17, by haftmann
slight improvement in serializer, stub for code generator theorems added
2006-03-17, by haftmann
Renamed setsum_mult to setsum_right_distrib.
2006-03-17, by ballarin
Internal restructuring: local parameters.
2006-03-17, by ballarin
renamed op < <= to Orderings.less(_eq)
2006-03-17, by haftmann
New interface function parameters_of_expr.
2006-03-16, by ballarin
add_inst_arity_i renamed to prove_arity.
2006-03-15, by berghofe
rename_frees: treat trivial names;
2006-03-15, by wenzelm
added singleton;
2006-03-14, by wenzelm
updated;
2006-03-14, by wenzelm
turned string_of_mixfix into pretty_mixfix;
2006-03-14, by wenzelm
added monomorphic;
2006-03-14, by wenzelm
added 'print_statement' command;
2006-03-14, by wenzelm
added print_stmts;
2006-03-14, by wenzelm
added pretty_statement;
2006-03-14, by wenzelm
added command, keyword;
2006-03-14, by wenzelm
Output.add_mode: keyword component;
2006-03-14, by wenzelm
string_of_mixfix;
2006-03-14, by wenzelm
print_statement;
2006-03-14, by wenzelm
added remove_trrules(_i);
2006-03-14, by wenzelm
added is_elim (from Provers/classical.ML);
2006-03-14, by wenzelm
added 'no_translations';
2006-03-14, by wenzelm
added pretty_stmt;
2006-03-14, by wenzelm
declared_const: check for type constraint only, i.e. admit abbreviations as well;
2006-03-14, by wenzelm
ObjectLogic.is_elim;
2006-03-14, by wenzelm
tuned constdecl;
2006-03-14, by wenzelm
updated;
2006-03-14, by wenzelm
Pure: no_translations;
2006-03-14, by wenzelm
refined representation of instance dictionaries
2006-03-14, by haftmann
entry for Library/AssocList
2006-03-13, by schirmer
First version of function for defining graph of iteration combinator.
2006-03-13, by berghofe
got rid of type Sign.sg;
2006-03-11, by wenzelm
renamed plus to add;
2006-03-11, by wenzelm
renamed const minus to subtract;
2006-03-11, by wenzelm
simplified AxClass interfaces;
2006-03-11, by wenzelm
added axclass_instance_XXX (from axclass.ML);
2006-03-11, by wenzelm
*** empty log message ***
2006-03-11, by wenzelm
added read_class, read/cert_classrel/arity (from axclass.ML);
2006-03-11, by wenzelm
moved read_class, read/cert_classrel/arity to sign.ML;
2006-03-11, by wenzelm
use axclass.ML earlier (in Isar/ROOT.ML);
2006-03-11, by wenzelm
nbe: no_document;
2006-03-11, by wenzelm
tuned;
2006-03-10, by wenzelm
exporting reapAll and killChild
2006-03-10, by paulson
text delimiter fixed
2006-03-10, by webertj
comment delimiter fixed
2006-03-10, by webertj
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
2006-03-10, by webertj
fix for document preparation
2006-03-10, by haftmann
Added Library/AssocList.thy
2006-03-10, by schirmer
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
2006-03-10, by haftmann
Changed some warnings to debug messages
2006-03-10, by paulson
Frequency analysis of constants (with types).
2006-03-10, by paulson
Shortened the exception messages from assume.
2006-03-10, by mengj
METAHYPS catches THM assume exception and prints out the terms containing schematic vars.
2006-03-10, by mengj
added many simple lemmas
2006-03-10, by huffman
Added more functions to the signature and tidied up some functions.
2006-03-09, by mengj
tuned;
2006-03-08, by wenzelm
tuned some proofs
2006-03-08, by urbanc
select_goals: split original conjunctions;
2006-03-08, by wenzelm
method: goal restriction defaults to [1];
2006-03-08, by wenzelm
infer_derivs: avoid allocating empty MinProof;
2006-03-08, by wenzelm
tuned;
2006-03-08, by wenzelm
Isar/method: goal restriction;
2006-03-08, by wenzelm
constdecl: always allow 'where';
2006-03-08, by wenzelm
deleted some proofs "on comment"
2006-03-08, by urbanc
tuned some proofs
2006-03-08, by urbanc
tuned some of the proofs about fresh_fun
2006-03-08, by urbanc
first running version of type classes
2006-03-08, by haftmann
first running version of type classes
2006-03-08, by haftmann
first running version of type classes
2006-03-08, by haftmann
Frequency strategy. Revised indentation, etc.
2006-03-08, by paulson
*** empty log message ***
2006-03-08, by nipkow
added ROOT.ML
2006-03-07, by obua
Indentation
2006-03-07, by paulson
Tidying and restructuring.
2006-03-07, by paulson
Tidying and tracing. Handling exn CLAUSE so that errors don't reach top-level.
2006-03-07, by paulson
Tidying. clausify_rules_pairs_abs now returns clauses in the same order as before.
2006-03-07, by paulson
Tidying. New invoke_atp_ml for top-level debugging. Flag to force FOL mode.
2006-03-07, by paulson
Tidying, and getting rid of SELECT_GOAL (as it does something different now)
2006-03-07, by paulson
Added HOL-ZF to Isabelle.
2006-03-07, by obua