Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-768
+768
+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.
avoid unqualified exception;
2006-06-11, by wenzelm
added quoting via back quotes
2006-06-11, by nipkow
updated IsaMakefiles for new location of IsaPlanner.
2006-06-11, by dixon
removed IsaPlanner - these are now in Provers.
2006-06-11, by dixon
removed IsaPlannner things from Pure. Moved to Provers.
2006-06-11, by dixon
moved to new location in Provers.
2006-06-11, by dixon
added updated version of IsaPlanner and substitution.
2006-06-11, by dixon
unique_names no longer set to false (thanks to improved naming
2006-06-09, by berghofe
- Changed naming scheme: names of "internal" constructors now have
2006-06-09, by berghofe
nbe -> NormalForm
2006-06-09, by nipkow
CVS: ----------------------------------------------------------------------
2006-06-09, by webertj
renamed command
2006-06-09, by nipkow
renamed file
2006-06-09, by nipkow
Removed "code del" declarations again.
2006-06-08, by berghofe
fixed owner bug
2006-06-08, by haftmann
less_equal -> less_eq (someone had screwd up here)
2006-06-08, by nipkow
Splitting order changed.
2006-06-08, by chaieb
added John's example
2006-06-08, by nipkow
replaced REPEAT by REPOEAT_DETERM
2006-06-08, by nipkow
gmake vs. make
2006-06-08, by haftmann
removed obsolete ML files;
2006-06-07, by wenzelm
removed obsolete ML files;
2006-06-07, by wenzelm
removed obsolete ML files;
2006-06-07, by wenzelm
adding case theorems for code generator
2006-06-07, by haftmann
slight code generator cleanup
2006-06-07, by haftmann
removed 'primitive definitions' added (non)strict generation, minor fixes
2006-06-07, by haftmann
fixed typo
2006-06-07, by haftmann
* Theory syntax: some popular names (e.g. "class", "if") are now keywords.
2006-06-07, by wenzelm
Schematic invocation of locale expression in proof context.
2006-06-07, by wenzelm
added invoke.ML;
2006-06-07, by wenzelm
added locale_insts;
2006-06-07, by wenzelm
renamed Type.(un)varifyT to Logic.(un)varifyT;
2006-06-07, by wenzelm
added 'if' and 'for' keywords;
2006-06-07, by wenzelm
added facts_of;
2006-06-07, by wenzelm
added Tools/invoke.ML;
2006-06-07, by wenzelm
renamed Type.(un)varifyT to Logic.(un)varifyT;
2006-06-07, by wenzelm
do not open Logic;
2006-06-07, by wenzelm
tuned;
2006-06-07, by wenzelm
removed obsolete ML files;
2006-06-07, by wenzelm
removed obsolete ML files;
2006-06-07, by wenzelm
removed obsolete ML files;
2006-06-07, by wenzelm
removed Toplevel.debug;
2006-06-06, by wenzelm
added zip_options;
2006-06-06, by wenzelm
tuned;
2006-06-06, by wenzelm
updated;
2006-06-06, by wenzelm
quoted "if";
2006-06-06, by wenzelm
added type inference at the end of normalization
2006-06-06, by nipkow
revised nbe command and examples
2006-06-06, by nipkow
new lemmas concerning finite cardinalities
2006-06-06, by paulson
quoted "if";
2006-06-06, by wenzelm
refined code generation
2006-06-06, by haftmann
added arbitray setup for codegen 2
2006-06-06, by haftmann
small fix
2006-06-06, by haftmann
deleted legacy
2006-06-06, by haftmann
improved code lemmas
2006-06-06, by haftmann
fixed typo
2006-06-06, by haftmann
bugfixes
2006-06-06, by haftmann
HOL/Tools/function_package: Applies CodeGen attributes again, where possible.
2006-06-06, by krauss
Improved parameter management of locales.
2006-06-06, by ballarin
HOL/Tools/function_package: imporoved handling of guards, added an example
2006-06-06, by krauss
HOL/Tools/function_package: More cleanup
2006-06-06, by krauss
export read/cert_expr;
2006-06-05, by wenzelm
guess: more careful about local polymorphism;
2006-06-05, by wenzelm
assm_tac: try rule termI;
2006-06-05, by wenzelm
added params_of, prems_of;
2006-06-05, by wenzelm
added matches_seq (left-to-right matching, intermediate beta-normalization);
2006-06-05, by wenzelm
support embedded terms;
2006-06-05, by wenzelm
allow non-trivial schematic goals (via embedded term vars);
2006-06-05, by wenzelm
HOL/Tools/fundef_package: Cleanup
2006-06-05, by krauss
added some further lemmas that deal with permutations and set-operators
2006-06-05, by urbanc
added the lemma perm_diff
2006-06-05, by urbanc
HOL/Tools/function_package: Added support for mutual recursive definitions.
2006-06-05, by krauss
Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure".
2006-06-05, by krauss
ATP/res_clasimpset.ML has been merged into res_atp.ML.
2006-06-04, by mengj
Functions of Tools/ATP/res_clasimpset.ML are now in Tools/res_atp.ML. res_clasimpset.ML is not used anymore.
2006-06-04, by mengj
generalized wfI
2006-06-03, by paulson
misc cleanup;
2006-06-02, by wenzelm
removed obsolete ML files;
2006-06-02, by wenzelm
tuned;
2006-06-02, by wenzelm
tuned;
2006-06-02, by wenzelm
removed obsolete ML files;
2006-06-02, by wenzelm
merge: always normalize (and check!) reductions;
2006-06-02, by wenzelm
removed legacy ML scripts
2006-06-01, by huffman
tuned;
2006-06-01, by wenzelm
removed obsolete ML files;
2006-06-01, by wenzelm
lemmas strip;
2006-06-01, by wenzelm
removed obsolete ML files;
2006-06-01, by wenzelm
added some installation notes for the nominal package
2006-06-01, by urbanc
Tiny code cleanup
2006-06-01, by paulson
added an example suggested by D. Wang on the PoplMark-mailing list;
2006-06-01, by urbanc
added the hack "reset NameSpace.unique_names" to Nominal.thy
2006-06-01, by urbanc
tuned type print-translations
2006-05-30, by schirmer
proper meta definition;
2006-05-29, by wenzelm
fixed bug in type print translations
2006-05-29, by schirmer
tuned;
2006-05-29, by wenzelm
warnings to debug outputs
2006-05-29, by paulson
warnings to debug outputs; default translation to const-typed
2006-05-29, by paulson
Giving the "--silent" switch to E, to produce less output
2006-05-29, by paulson
fixing a variable-clash bug in rule_by_tactic
2006-05-29, by paulson
removed legacy ML scripts;
2006-05-28, by wenzelm
removed legacy ML scripts;
2006-05-28, by wenzelm
removed legacy ML scripts;
2006-05-27, by wenzelm
removed legacy ML scripts;
2006-05-27, by wenzelm
removed legacy ML scripts;
2006-05-27, by wenzelm
tuned;
2006-05-27, by wenzelm
tuned;
2006-05-27, by wenzelm
complete_split_rule: all Vars;
2006-05-27, by wenzelm
unfold/refold: LocalDefs.meta_rewrite_rule;
2006-05-27, by wenzelm
removed unused extern_thm;
2006-05-26, by wenzelm
activate Defines: fix frees;
2006-05-26, by wenzelm
pretty: do not exterm thm names;
2006-05-26, by wenzelm
forall_intr_list: do not ignore errors;
2006-05-26, by wenzelm
separate checks for acyclic/wellformed;
2006-05-26, by wenzelm
freeze_spec: gensym;
2006-05-26, by wenzelm
tuned;
2006-05-25, by wenzelm
axiomatization java_lang;
2006-05-25, by wenzelm
Changed the DFG format's functions' declaration procedure.
2006-05-25, by mengj
Fixed a bug.
2006-05-25, by mengj
A new "spass" method.
2006-05-25, by mengj
Added in settings used by "spass" method.
2006-05-25, by mengj
Added in SPASS oracle.
2006-05-25, by mengj
HOL problems now have DFG output format.
2006-05-25, by mengj
Changed input interface of dfg_write_file.
2006-05-25, by mengj
Added support for DFG format, used by SPASS.
2006-05-25, by mengj
Helper files in DFG format.
2006-05-25, by mengj
add_datatype_axm: finalize specified consts;
2006-05-24, by wenzelm
tuned;
2006-05-24, by wenzelm
tuned;
2006-05-24, by wenzelm
made smlnj happy;
2006-05-24, by wenzelm
wellformed: be less ambitious about structural containment;
2006-05-24, by wenzelm
Pure: update on overloaded defs;
2006-05-24, by wenzelm
Extended strong induction rule with additional
2006-05-24, by berghofe
add theorem cfcomp_strict
2006-05-24, by huffman
added add_deps, which actually records dependencies of consts (unlike add_finals);
2006-05-24, by wenzelm
tuned;
2006-05-24, by wenzelm
axiomatize class: Theory.add_deps;
2006-05-24, by wenzelm
simplified info/get_info;
2006-05-24, by wenzelm
simplified TypedefPackage.get_info;
2006-05-24, by wenzelm
made smlnj happy;
2006-05-23, by wenzelm
pretty_full_theory: tuned output of definitions;
2006-05-23, by wenzelm
export plain_args;
2006-05-23, by wenzelm
Defs.specifications_of: lhs/rhs now use typargs;
2006-05-22, by wenzelm
removed unchecked'';
2006-05-22, by wenzelm
pretty_full_theory: defs;
2006-05-22, by wenzelm
specifications_of: lhs/rhs represented as typargs;
2006-05-22, by wenzelm
export raw_unifys, could_unifys;
2006-05-22, by wenzelm
made smlnj happy;
2006-05-20, by wenzelm
export raw_matches;
2006-05-20, by wenzelm
tuned Defs interfaces;
2006-05-20, by wenzelm
yet another re-implementation:
2006-05-20, by wenzelm
removed obsolete partition (cf. List.partition);
2006-05-20, by wenzelm
class axiomatization: finals;
2006-05-20, by wenzelm
abs: precise typing;
2006-05-20, by wenzelm
added syntax for 'unchecked';
2006-05-20, by wenzelm
primrec (unchecked);
2006-05-20, by wenzelm
List.partition;
2006-05-20, by wenzelm
ax_derivs: precise typing;
2006-05-20, by wenzelm
pow: unchecked;
2006-05-20, by wenzelm
removed obsolete 'finalconsts';
2006-05-20, by wenzelm
* Pure: syntax 'CONST name' produces a fully internalized constant;
2006-05-17, by wenzelm
added CONST syntax;
2006-05-17, by wenzelm
export generic term_syntax;
2006-05-17, by wenzelm
consts: replaced early'' flag by inverted authentic'';
2006-05-17, by wenzelm
added mapping;
2006-05-17, by wenzelm
replaced early'' flag by inverted authentic'';
2006-05-17, by wenzelm
renamed CONST to CONSTANT;
2006-05-17, by wenzelm
removing the string array from the result of get_clasimp_atp_lemmas
2006-05-17, by paulson
const_syntax;
2006-05-17, by wenzelm
always preserve authentic consts -- removed Syntax.mixfix_const;
2006-05-17, by wenzelm
tuned;
2006-05-17, by wenzelm
removed outdated/redundant comments;
2006-05-17, by wenzelm
prefer 'definition' over low-level defs;
2006-05-17, by wenzelm
tuned source/document;
2006-05-17, by wenzelm
hide const subst;
2006-05-16, by wenzelm
tuned;
2006-05-16, by wenzelm
const_syntax;
2006-05-16, by wenzelm
* Isar/locale: 'const_syntax';
2006-05-16, by wenzelm
added const_syntax(_i);
2006-05-16, by wenzelm
export consts_of;
2006-05-16, by wenzelm
replaced abbrevs by term_syntax, which is both simpler and more general;
2006-05-16, by wenzelm
added syntax interface;
2006-05-16, by wenzelm
added add_modesyntax;
2006-05-16, by wenzelm
added 'const_syntax';
2006-05-16, by wenzelm
added add_const_syntax, add_consts_authentic;
2006-05-16, by wenzelm
added syntax interface;
2006-05-16, by wenzelm
tuned concrete syntax -- abbreviation/const_syntax;
2006-05-16, by wenzelm
updated;
2006-05-16, by wenzelm
updated;
2006-05-16, by wenzelm
* Pure/library: divide_and_conquer;
2006-05-16, by wenzelm
replaced references to the robot by the mailing list page
2006-05-16, by paulson
added a much simpler proof for the iteration and
2006-05-16, by urbanc
Amine Chaieb: Ferrante and Rackoff Algorithm;
2006-05-16, by wenzelm
Sign.certify_sort;
2006-05-16, by wenzelm
tuned;
2006-05-16, by wenzelm
removed low-level str_of_sort/typ/term (use Display.raw_string_of_sort/typ/term instead, or even PolyML.print -- for debugging purposes);
2006-05-16, by wenzelm
avoid low-level Term.str_of_term;
2006-05-16, by wenzelm
abstract interfaces for type algebra;
2006-05-16, by wenzelm
added divide_and_conquer combinator (by Amine Chaieb);
2006-05-16, by wenzelm
added low-level string_of_term (back again from term.ML) -- should avoid this altogether;
2006-05-16, by wenzelm
more abstract interface to classes/arities;
2006-05-16, by wenzelm
replaced low-level Term.str_of by Display.raw_string_of_term (should actually use Display.string_of_term);
2006-05-16, by wenzelm
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
2006-05-16, by wenzelm
fixed handling of absolute urls
2006-05-16, by haftmann
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
2006-05-15, by urbanc
reactivated translations for less/less_eq;
2006-05-13, by wenzelm
added add_primrec_unchecked_i;
2006-05-13, by wenzelm
unchecked definitions;
2006-05-13, by wenzelm
defs (unchecked overloaded), including former primrec;
2006-05-13, by wenzelm
updated;
2006-05-13, by wenzelm
add_defs: unchecked flag;
2006-05-13, by wenzelm
'defs': unchecked flag;
2006-05-13, by wenzelm
Theory.add_defs(_i): added unchecked flag;
2006-05-13, by wenzelm
added add_defs_unchecked(_i);
2006-05-13, by wenzelm
actually reject malformed defs;
2006-05-13, by wenzelm
moved defs explanation to isar-ref;
2006-05-13, by wenzelm
added defs (unchecked)'';
2006-05-13, by wenzelm
* Pure: overloaded definitions are now actually checked for acyclic dependencies;
2006-05-13, by wenzelm
tuned;
2006-05-12, by wenzelm
added lemma in_measure
2006-05-12, by nipkow
fixed silly bug in function serializer for ML
2006-05-12, by haftmann
add new finite chain theorems
2006-05-12, by huffman
improved propagate_deps;
2006-05-12, by wenzelm
check result against certified prop, i.e. admit non-normal statements;
2006-05-11, by wenzelm
tuned;
2006-05-11, by wenzelm
avoid raw equality on type thm;
2006-05-11, by wenzelm
replaced Graph.fold_nodes by general Graph.fold;
2006-05-11, by wenzelm
added fold;
2006-05-11, by wenzelm
tuned Defs.merge;
2006-05-11, by wenzelm
allow dependencies of disjoint collections of instances;
2006-05-11, by wenzelm
use IntGraph from Pure;
2006-05-11, by wenzelm
Function Package: Quick-and-dirty-fixed strange "Proved a different theorem bug"
2006-05-11, by krauss
Fix: Auto term must apply wf-intro rules repeatedly.
2006-05-11, by krauss
fixed codegen bug, cleanup
2006-05-11, by haftmann
revert accidental text change;
2006-05-10, by wenzelm
introduced characters for code generator; some improved code lemmas for some list functions
2006-05-09, by haftmann
added .cvsignore
2006-05-09, by haftmann
added ExecutableRat.thy
2006-05-09, by haftmann
removed 1::int
2006-05-09, by haftmann
added preprocs for CodegenTheorems
2006-05-09, by haftmann
improved code generation for wfrec
2006-05-09, by haftmann
added codegen preprocessors for numerals
2006-05-09, by haftmann
adaption to CodegenTheorems
2006-05-09, by haftmann
added DatatypeHooks
2006-05-09, by haftmann
different object logic setup for CodegenTheorems
2006-05-09, by haftmann
major refinement of codegen_theorems.ML
2006-05-09, by haftmann
removed superfluous eq_ord
2006-05-09, by haftmann
improved chmod/chgrp handling
2006-05-09, by haftmann
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
2006-05-08, by huffman
quoted 'termination' command;
2006-05-08, by wenzelm
Defs.define: const_typargs;
2006-05-08, by wenzelm
added raw_string_of_sort/typ/term;
2006-05-08, by wenzelm
simple substructure test for typargs (independent type constructors);
2006-05-08, by wenzelm
tuned;
2006-05-08, by wenzelm
string_of_option tuned
2006-05-08, by webertj
* Isar: removed obsolete 'concl is' patterns.
2006-05-07, by wenzelm
removed 'concl is' pattern;
2006-05-07, by wenzelm
removed 'concl is' patterns;
2006-05-07, by wenzelm
tuned;
2006-05-07, by wenzelm
function-package: Changed record usage to make sml/nj happy...
2006-05-07, by krauss
get rid of 'concl is';
2006-05-05, by wenzelm
more robust pretty_term_typ, using well-typed parse tree representation;
2006-05-05, by wenzelm
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
2006-05-05, by wenzelm
replaced Sorts.DOMAIN by general Sorts.CLASS_ERROR;
2006-05-05, by wenzelm
added class_error and exception CLASS_ERROR (supercedes DOMAIN);
2006-05-05, by wenzelm
added syntax for _type_constraint_;
2006-05-05, by wenzelm
extern_early: improved handling of undeclared constants;
2006-05-05, by wenzelm
replaced Graph.find_paths by Graph.irreducible_paths;
2006-05-05, by wenzelm
of_sort: explicit cache value;
2006-05-05, by wenzelm
axiomatization;
2006-05-05, by wenzelm
* Library: theory Accessible_Part has been move to main HOL.
2006-05-05, by wenzelm
Theory.definitions_of;
2006-05-05, by wenzelm
added definitions_of;
2006-05-05, by wenzelm
specifications_of: more detailed information;
2006-05-05, by wenzelm
Added small example theory for new function package.
2006-05-05, by krauss
string_of_... functions added
2006-05-05, by webertj
added the lemma pt_fresh_bij2
2006-05-05, by urbanc
added something
2006-05-05, by haftmann
First usable version of the new function definition package (HOL/function_packake/...).
2006-05-05, by krauss
added something
2006-05-05, by haftmann
added the lemma abs_fun_eq' to the nominal theory,
2006-05-05, by urbanc
extensive reformatting and cleaning up code (no changes in functionality)
2006-05-05, by huffman
slight fix
2006-05-04, by haftmann
added world map
2006-05-04, by haftmann
added js
2006-05-04, by haftmann
Rat.one added
2006-05-04, by webertj
fixed some flaws
2006-05-04, by haftmann
fixed some flaws
2006-05-04, by haftmann
added world map
2006-05-03, by haftmann
pre_cnf_tac: beta-eta-normalization restricted to the current subgoal
2006-05-03, by webertj
improvments in mail obfuscator
2006-05-03, by haftmann
converted to isar theory; removed unsound adm_all axiom
2006-05-03, by huffman
update to reflect changes in inverts/injects lemmas
2006-05-03, by huffman
inverts and injects generated lemmas now take the form of rewrite rules, instead of dest rules
2006-05-03, by huffman
added lemma fresh_right, which is useful
2006-05-03, by urbanc
added the_theory;
2006-05-02, by wenzelm
extend/remove_syntax: observe inout flag for translations, too;
2006-05-02, by wenzelm
handle exception SYS_ERROR;
2006-05-02, by wenzelm
abbreviation: observe local syntax mode;
2006-05-02, by wenzelm
added set_syntax_mode, restore_syntax_mode;
2006-05-02, by wenzelm
sys_error: exception SYS_ERROR;
2006-05-02, by wenzelm
maintain implicit syntax mode;
2006-05-02, by wenzelm
ThyInfo.the_theory;
2006-05-02, by wenzelm
ThyInfo.the_theory;
2006-05-02, by wenzelm
actually removed old stuff;
2006-05-02, by wenzelm
replaced syntax/translations by abbreviation;
2006-05-02, by wenzelm
replaced syntax/translations by abbreviation;
2006-05-02, by wenzelm
replaced syntax/translations by abbreviation;
2006-05-02, by wenzelm
beta_eta_conversion added to pre_cnf_tac
2006-05-02, by webertj
added obfuscation for mails
2006-05-02, by haftmann
tidied and harmonized "params_of_state"
2006-05-02, by paulson
tuned;
2006-05-02, by wenzelm
tuned;
2006-05-02, by wenzelm
added domain_error;
2006-05-02, by wenzelm
of_sort: option;
2006-05-02, by wenzelm
some facts about min, max and add, diff
2006-05-01, by paulson
a few more examples
2006-05-01, by paulson
class_triv: Sign.certify_class;
2006-05-01, by wenzelm
arities: maintain original codomain;
2006-05-01, by wenzelm
added sort_triv;
2006-05-01, by wenzelm
of_sort: simplified derivation;
2006-05-01, by wenzelm
adapted arities;
2006-05-01, by wenzelm
add theorem flift2_defined_iff
2006-05-01, by huffman
add theorem typdef_flat
2006-05-01, by huffman
AxClass.define_class_i, AxClass.get_definition;
2006-04-30, by wenzelm
tuned;
2006-04-30, by wenzelm
AxClass.define_class;
2006-04-30, by wenzelm
build classes/arities: refer to operations in sorts.ML;
2006-04-30, by wenzelm
moved certify_class/sort to type.ML;
2006-04-30, by wenzelm
removed add_classes/classrel/arities (superceded by AxClass.axiomatize_class/classrel/arity);
2006-04-30, by wenzelm
added serial_string;
2006-04-30, by wenzelm
renamed add_axclass(_i) to define_axclass(_i);
2006-04-30, by wenzelm
AxClass.axiomatize_arity_i;
2006-04-30, by wenzelm
AxClass.define_class_i;
2006-04-30, by wenzelm
* Pure: axclasses now purely definitional;
2006-04-30, by wenzelm
reduced code duplication;
2006-04-29, by wenzelm
added insert_list;
2006-04-29, by wenzelm
added unconstrainT;
2006-04-29, by wenzelm
added unconstrainTs;
2006-04-29, by wenzelm
instances data: mutable cache;
2006-04-29, by wenzelm
tuned;
2006-04-29, by wenzelm
Capitalized theory names.
2006-04-28, by berghofe
Removed broken proof.
2006-04-28, by berghofe
Added Class, Fsub, and Lambda_mu examples for nominal datatypes.
2006-04-28, by berghofe
New keyword file for HOL nominal datatype package.
2006-04-28, by berghofe
Added new targets for nominal datatype package.
2006-04-28, by berghofe
Capitalized theory names.
2006-04-28, by berghofe
New ROOT file for nominal datatype examples.
2006-04-28, by berghofe
Renamed "nominal" theory to "Nominal".
2006-04-28, by berghofe
New ROOT file for nominal datatype package.
2006-04-28, by berghofe
added some helper files for HOL goals/lemmas. Clauses have TPTP format.
2006-04-28, by mengj
changed the functions for getting HOL helper clauses.
2006-04-28, by mengj
removed the functions for getting HOL helper paths.
2006-04-28, by mengj
SplitAt -> chop
2006-04-27, by berghofe
Adapted to new interface of add_axclass_i.
2006-04-27, by berghofe
added zip/take/drop lemmas
2006-04-27, by nipkow
tuned;
2006-04-27, by wenzelm
renamed Source.mapfilter to Source.map_filter;
2006-04-27, by wenzelm
added map_filter;
2006-04-27, by wenzelm
renamed mapfilter to map_filter, made pervasive (again);
2006-04-27, by wenzelm
tuned basic list operators (flat, maps, map_filter);
2006-04-27, by wenzelm
renamed HOLogic.mk_bin to mk_binum for consistency with dest_binum
2006-04-27, by paulson
slight shortening of blacklist
2006-04-27, by paulson
cosmetic changes
2006-04-27, by paulson
some new functions
2006-04-27, by paulson
isar-keywords.el
2006-04-27, by urbanc
*** empty log message ***
2006-04-26, by wenzelm
curried Seq.cons;
2006-04-26, by wenzelm
removed splitAt (superceded by chop);
2006-04-26, by wenzelm
tuned;
2006-04-26, by wenzelm
removed obsolete expand_case_tac;
2006-04-26, by wenzelm
fixed silly symlink bug
2006-04-26, by haftmann
added Ben Porter's stuff
2006-04-26, by kleing
moved arithmetic series to geometric series in SetInterval
2006-04-26, by kleing
Sign.arity_sorts;
2006-04-25, by wenzelm
unlocalize_mixfix: fallback on NoSyn;
2006-04-25, by wenzelm
tuned;
2006-04-25, by wenzelm
refer to structure Type instead of Sorts;
2006-04-25, by wenzelm
added inter_sort;
2006-04-25, by wenzelm
added remove_sort;
2006-04-25, by wenzelm
added arity_number/sorts;
2006-04-25, by wenzelm
made 'flat' pervasive (again);
2006-04-25, by wenzelm
get_info: removed 'super' field;
2006-04-25, by wenzelm
seperated typedef codegen from main code
2006-04-24, by haftmann
more precise tactics
2006-04-24, by haftmann
fixed typo
2006-04-24, by haftmann
more precise data structure
2006-04-24, by haftmann
cleaned up some diagnostic mathom
2006-04-24, by haftmann
moved coalesce to AList, added equality predicates to library
2006-04-24, by haftmann
added LP.thy
2006-04-23, by obua
Changed the treatment of equalities.
2006-04-22, by mengj
Changed the logic detection method.
2006-04-20, by mengj
exported linkup_logic_mode and changed the default setting
2006-04-19, by paulson
fix to spacing in switches, for Vampire under SML/NJ
2006-04-19, by paulson
definition expansion checks for excess variables
2006-04-19, by paulson
the "th" field of type "clause"
2006-04-19, by paulson
tidying and reformatting
2006-04-19, by paulson
tidying; ATP options including CASC mode for Vampire
2006-04-19, by paulson
Take conjectures and axioms as thms when convert them to ResHolClause.clause format.
2006-04-18, by mengj
Take conjectures and axioms as thms when convert them to ResClause.clause format.
2006-04-18, by mengj
Tidied up some programs.
2006-04-18, by mengj
fixed typo
2006-04-16, by haftmann
add lemma less_UU_iff as default simp rule
2006-04-13, by huffman
hide common name of constant 'run'
2006-04-13, by huffman
early test of Classpackage, Codegenerator;
2006-04-13, by wenzelm
fixed typo in method invocation;
2006-04-13, by wenzelm
ignore sort constraints of consts declarations;
2006-04-13, by wenzelm
ignore sort constraints of consts declarations;
2006-04-13, by wenzelm
add_axclass(_i): canonical specification format;
2006-04-13, by wenzelm
certify: ignore sort constraints of declarations (MAJOR CHANGE);
2006-04-13, by wenzelm
added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
2006-04-13, by wenzelm
axclass: old-style concrete syntax for canonical specification format;
2006-04-13, by wenzelm
ProofDisplay.print_theorems/theory;
2006-04-13, by wenzelm
added maxidx_of;
2006-04-13, by wenzelm
tuned;
2006-04-13, by wenzelm
added typ_equiv;
2006-04-13, by wenzelm
moved print_theorems/theory to Isar/proof_display.ML;
2006-04-13, by wenzelm
added dest_conjunction_list;
2006-04-13, by wenzelm
export unflat (again);
2006-04-13, by wenzelm
use conjunction stuff from conjunction.ML;
2006-04-13, by wenzelm
expand_atom: Type.raw_match;
2006-04-13, by wenzelm
added equal_elim_rule2;
2006-04-13, by wenzelm
tuned comment;
2006-04-13, by wenzelm
ignore sorts of consts declarations;
2006-04-13, by wenzelm
reworded add_axclass(_i): canonical specification format,
2006-04-13, by wenzelm
added conjunction.ML;
2006-04-13, by wenzelm
Meta-level conjunction.
2006-04-13, by wenzelm
added conjunction.ML;
2006-04-13, by wenzelm
Sign.typ_equiv;
2006-04-13, by wenzelm
added subversion treatment
2006-04-13, by haftmann
classes: prefer thy operations;
2006-04-11, by wenzelm
export pretty_classrel/arity;
2006-04-11, by wenzelm
'axclass': no parameters;
2006-04-11, by wenzelm
tuned;
2006-04-11, by wenzelm
removed superclasses (see sign.ML);
2006-04-11, by wenzelm
added super_classes (from sorts.ML);
2006-04-11, by wenzelm
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
2006-04-11, by wenzelm
moved abstract syntax operations to logic.ML;
2006-04-11, by wenzelm
Moved stuff from Ring_and_Field to Matrix
2006-04-10, by obua
Adapted to changed type of add_typedef_i.
2006-04-10, by berghofe
Hoare(Parallel) dependencies on document/*
2006-04-10, by nipkow
added references
2006-04-10, by nipkow
Minimal doc
2006-04-10, by nipkow
Included cyclic list examples
2006-04-10, by nipkow
fixed value restriction
2006-04-10, by haftmann
Added splicing algorithm.
2006-04-10, by nipkow
hide (open) const;
2006-04-10, by wenzelm
simplified AxClass.add_axclass interface;
2006-04-10, by wenzelm
added aT (from axclass.ML);
2006-04-10, by wenzelm
removed unused class_le_path, sort_less;
2006-04-10, by wenzelm
add_axclass(_i): return class name only;
2006-04-10, by wenzelm
Term.itselfT;
2006-04-10, by wenzelm
Added function "splice"
2006-04-09, by nipkow
Even/Odd: avoid clash with even/odd of Main HOL;
2006-04-09, by wenzelm
results: smart_pretty_thm uses adhoc proof context if possible;
2006-04-09, by wenzelm
added full_name;
2006-04-09, by wenzelm
add_syntax: actually observe print mode;
2006-04-09, by wenzelm
print_term etc.: actually observe print mode in final output;
2006-04-09, by wenzelm
abbrevs: mode does not affect name space;
2006-04-09, by wenzelm
added coalesce;
2006-04-09, by wenzelm
moved theory presentation to Isar/ROOT.ML;
2006-04-09, by wenzelm
hide consts in Numeral.thy;
2006-04-09, by wenzelm
tuned syntax/abbreviations;
2006-04-09, by wenzelm
unfold(ed): not necessrily meta equations;
2006-04-09, by wenzelm
Made "empty" an abbreviation.
2006-04-09, by nipkow
*** empty log message ***
2006-04-09, by nipkow
Removed old set interval syntax.
2006-04-09, by nipkow
pretty_term: late externing of consts (support authentic syntax);
2006-04-08, by wenzelm
pretty: late externing of consts (support authentic syntax);
2006-04-08, by wenzelm
removed fix_mixfix;
2006-04-08, by wenzelm
abbreviation(_i): do not expand abbreviations, do not use derived_def;
2006-04-08, by wenzelm
add_abbrevs(_i): support print mode;
2006-04-08, by wenzelm
abbrevs: support print mode;
2006-04-08, by wenzelm
simplified handling of authentic syntax (cf. early externing in consts.ML);
2006-04-08, by wenzelm
'abbreviation': optional print mode;
2006-04-08, by wenzelm
tuned;
2006-04-08, by wenzelm
pretty_term': early vs. late externing (support authentic syntax);
2006-04-08, by wenzelm
print_theory: print abbreviations nicely;
2006-04-08, by wenzelm
added intern/extern/extern_early;
2006-04-08, by wenzelm
refined 'abbreviation';
2006-04-08, by wenzelm
made symlink relative
2006-04-08, by haftmann
made symlink relative
2006-04-08, by haftmann
converted Müller to Mueller to make smlnj 110.58 work
2006-04-08, by kleing
Fixed bug that caused proof of induction rule to fail
2006-04-07, by berghofe
remame ASeries to Arithmetic_Series
2006-04-07, by kleing
Added alternative version of thms_of_proof that does not recursively
2006-04-07, by berghofe
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
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
substantial improvement in codegen iml
2006-03-07, by haftmann
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
2006-03-07, by mengj
relevance_filter takes input axioms as Term.term.
2006-03-07, by mengj
Proof reconstruction now only takes names of theorems as input.
2006-03-07, by mengj
Added tptp_write_file to write all necessary ATP input clauses to one file.
2006-03-07, by mengj
tptp_write_file now takes goals and axioms as Term.term and writes them to a file.
2006-03-07, by mengj
Added functions to retrieve local and global atpset rules.
2006-03-07, by mengj
Moved the settings for ATP time limit to res_atp.ML
2006-03-07, by mengj
Merged res_atp_setup.ML into res_atp.ML.
2006-03-07, by mengj
When ATP methods call ATPs, all input clauses from one subgoal are written to one file.
2006-03-07, by mengj
Merged res_atp_setup.ML into res_atp.ML.
2006-03-07, by mengj
SELECT_GOAL: fixed trivial case;
2006-03-05, by wenzelm
fixed a typo in a comment
2006-03-05, by webertj
tuned;
2006-03-04, by wenzelm
method: SelectGoals;
2006-03-04, by wenzelm
method: syntax for SelectGoals;
2006-03-04, by wenzelm
text: added SelectGoals;
2006-03-04, by wenzelm
tuned conj_curry;
2006-03-04, by wenzelm
added extract, retrofit;
2006-03-04, by wenzelm
added mk_conjunction;
2006-03-04, by wenzelm
method: restriction to first n sub-goals;
2006-03-04, by wenzelm
minor changes
2006-03-03, by nipkow
more examples
2006-03-03, by nipkow
changed and retracted change of location of code lemmas.
2006-03-03, by nipkow
ignore repeated vars on lhs, cleanup
2006-03-03, by nipkow
improvements for nbe
2006-03-03, by haftmann
reformatting
2006-03-02, by paulson
subset_refl now included using the atp attribute
2006-03-02, by paulson
moved the "use" directive
2006-03-02, by paulson
fixed the bugs itroduced by the previous commit
2006-03-02, by urbanc
made some small changes to generate nicer latex-output
2006-03-02, by urbanc
split the files
2006-03-02, by urbanc
Added in a signature.
2006-03-02, by mengj
fixed a problem where a permutation is not analysed
2006-03-01, by urbanc
streamlined the proof
2006-03-01, by urbanc
refined representation of codegen intermediate language
2006-03-01, by haftmann
some small tunings
2006-03-01, by urbanc
added fresh_fun_eqvt theorem to the theorem collection
2006-03-01, by urbanc
added initialisation-code for finite_guess
2006-03-01, by urbanc
made some small tunings in the decision-procedure
2006-03-01, by urbanc
Added setup for "atpset" (a rule set for ATPs).
2006-03-01, by mengj
Added file Tools/res_atpset.ML.
2006-03-01, by mengj
Merged HOL and FOL clauses and combined some functions.
2006-03-01, by mengj
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
2006-03-01, by mengj
some minor tuning on the proofs
2006-03-01, by urbanc
initial commit (especially 2nd half needs to be cleaned up)
2006-02-28, by urbanc
removal of theory blacklist
2006-02-28, by paulson
new order for arity clauses
2006-02-28, by paulson
fixed but in freeze_spec
2006-02-28, by paulson
splitting up METAHYPS into smaller functions
2006-02-28, by paulson
typos
2006-02-28, by paulson
added a finite_guess tactic, which solves
2006-02-27, by urbanc
class package and codegen refinements
2006-02-27, by haftmann
added nbe
2006-02-27, by haftmann
added temp. nbe test
2006-02-27, by nipkow
added nbe, updated neb_*
2006-02-27, by nipkow
added nbe
2006-02-27, by nipkow
Typo.
2006-02-27, by ballarin
added support for arbitrary atoms in the simproc
2006-02-27, by urbanc
put_thms: do_index;
2006-02-26, by wenzelm
rewrite_goals_rule_aux: actually use prems if present;
2006-02-26, by wenzelm
add_local: do_index;
2006-02-26, by wenzelm
replaced the lemma at_two by at_different;
2006-02-26, by urbanc
improved the decision-procedure for permutations;
2006-02-26, by urbanc
improved codegen bootstrap
2006-02-25, by haftmann
change in codegen syntax
2006-02-25, by haftmann
some refinements
2006-02-25, by haftmann
added more detailed data to consts
2006-02-25, by haftmann
Reverted to old interface of AxClass.add_inst_arity(_i)
2006-02-24, by berghofe
Adapted to Florian's recent changes to the AxClass package.
2006-02-24, by berghofe
added lemmas
2006-02-23, by urbanc
make SML/NJ happy;
2006-02-23, by wenzelm
Default type level is T_FULL now.
2006-02-23, by mengj
eprover removes tmp files too.
2006-02-23, by mengj
vampire/eprover methods can now be applied repeatedly until they fail.
2006-02-23, by mengj
removed obsolete meta_conjunction_tr';
2006-02-22, by wenzelm
rew: handle conjunctionI/D1/D2;
2006-02-22, by wenzelm
simplified Pure conjunction, based on actual const;
2006-02-22, by wenzelm
removed rename_indexes_wrt;
2006-02-22, by wenzelm
renamed class_axms to class_intros;
2006-02-22, by wenzelm
tuned proofs;
2006-02-22, by wenzelm
simplified Pure conjunction;
2006-02-22, by wenzelm
not_equal: replaced syntax translation by abbreviation;
2006-02-22, by wenzelm
abandoned merge_alists' in favour of generic AList.merge
2006-02-22, by haftmann
added Tools/nbe, fixes
2006-02-21, by nipkow
added Tools/nbe
2006-02-21, by nipkow
New normalization-by-evaluation package
2006-02-21, by nipkow
distinct (op =);
2006-02-21, by wenzelm
fixed
2006-02-20, by kleing
Inclusion of subset_refl in ATP calls
2006-02-20, by paulson
Fix variable-naming bug (?) by removing a needless recursive call
2006-02-20, by paulson
slight code generator serialization improvements
2006-02-20, by haftmann
moved intro_classes from AxClass to ClassPackage
2006-02-20, by haftmann
fixed document
2006-02-19, by kleing
* denumerability of rationals by Benjamin Porter, based on NatPair (by Stefan Richter)
2006-02-19, by kleing
added a few lemmas to do with permutation-equivalence for the
2006-02-19, by urbanc
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
2006-02-19, by kleing
use minimal imports
2006-02-19, by huffman
use qualified name for return
2006-02-19, by huffman
dest_def: tuned error msg;
2006-02-18, by wenzelm
const constraints: provide TFrees instead of TVars,
2006-02-17, by wenzelm
checkpoint/copy_node: reset body context;
2006-02-17, by wenzelm
global_qeds: transfer body context;
2006-02-17, by wenzelm
add_const_constraint(_i): demand TFrees instead of TVars, optional type (i.e. may delete constraints);
2006-02-17, by wenzelm
constrain: assert const declaration, optional type (i.e. may delete constraints);
2006-02-17, by wenzelm
removed Import/lazy_scan.ML;
2006-02-17, by wenzelm
hyperlinks in the PDF work now
2006-02-17, by paulson
replaced Symbol.explode by explode
2006-02-17, by obua
updated mailing list archive link
2006-02-17, by haftmann
use monomorphic sequences / scanners
2006-02-17, by obua
make maybe into a real type constructor; remove monad syntax
2006-02-17, by huffman
use VectorScannerSeq instead of ListScannerSeq in xml.ML
2006-02-16, by obua
removed lazy_scan
2006-02-16, by obua
improved scanning
2006-02-16, by obua
tuned;
2006-02-16, by wenzelm
Abstract Natural Numbers with polymorphic recursion.
2006-02-16, by wenzelm
new-style definitions/abbreviations;
2006-02-16, by wenzelm
added ex/Abstract_NAT.thy;
2006-02-16, by wenzelm
tuned;
2006-02-16, by wenzelm
tuned;
2006-02-16, by wenzelm
removed silly stuff
2006-02-16, by haftmann
* Isar/locales: new derived specification elements 'definition', 'abbreviation', 'axiomatization';
2006-02-16, by wenzelm
added abbreviation(_i);
2006-02-16, by wenzelm
added put_thms_internal: local_naming, no fact index;
2006-02-16, by wenzelm
added put_thms_internal;
2006-02-16, by wenzelm
added abbrev element;
2006-02-16, by wenzelm
added 'abbreviation';
2006-02-16, by wenzelm
added premsN;
2006-02-16, by wenzelm
Proof.put_thms_internal;
2006-02-16, by wenzelm
less
more
|
(0)
-10000
-3000
-1000
-768
+768
+1000
+3000
+10000
+30000
tip