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

hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.
2006-04-07, by mengj
filter now accepts axioms as thm, instead of term.
2006-04-07, by mengj
tptp_write_file accepts axioms as thm.
2006-04-07, by mengj
added another function for CNF.
2006-04-07, by mengj
lemmas returned from ResClasimp.get_clasimp_atp_lemmas are thm rather than term.
2006-04-07, by mengj
renamed ASeries to Arithmetic_Series, removed the ^M
2006-04-07, by kleing
modified the perm_compose rule such that it
2006-04-06, by urbanc
cleanup in typedef/datatype package
2006-04-06, by haftmann
added explicit serialization for int equality
2006-04-06, by haftmann
adapted for definitional code generation
2006-04-06, by haftmann
cleanup in datatype package
2006-04-06, by haftmann
small type annotation fix
2006-04-06, by haftmann
added hook for codegen_theorems.ML
2006-04-06, by haftmann
adaptions to change in typedef_package.ML
2006-04-06, by haftmann
added functions for definitional code generation
2006-04-06, by haftmann
added definitional code generator module: codegen_theorems.ML
2006-04-06, by haftmann
minor changes
2006-04-06, by haftmann
exported specification names
2006-04-06, by haftmann
minor extensions
2006-04-05, by haftmann
pool of constants; definition expansion; current best settings
2006-04-05, by paulson
removed some illegal characters: they were crashing SML/NJ
2006-03-31, by paulson
Removal of unused code
2006-03-31, by paulson
Simplified version of Jia's filter. Now all constants are pooled, rather than
2006-03-28, by paulson
renamed map_val to map_ran
2006-03-28, by schirmer
added map_val, superseding map_at and substitute
2006-03-28, by schirmer
some internal cleanup
2006-03-28, by haftmann
removed illegal character codes
2006-03-27, by paulson
simplified the proof at_fin_set_supp
2006-03-26, by urbanc
changed abbreviation for "infinite" back to translation because
2006-03-25, by nipkow
lazy patterns in lambda abstractions
2006-03-24, by huffman
changed the it_prm proof to work for recursion
2006-03-24, by urbanc
tuned some proofs
2006-03-24, by urbanc
Removed occurrences of makestring, which does not
2006-03-24, by berghofe
Converted translations to abbbreviations.
2006-03-23, by nipkow
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