Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-480
+480
+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.
fold_index replacing foldln
2005-10-31, by haftmann
A few new lemmas
2005-10-31, by nipkow
tuned my last commit
2005-10-30, by urbanc
simplified the abs_supp_approx proof and tuned some comments in
2005-10-30, by urbanc
Changed Simplifier.simp_modifiers to Simplifier.simp_modifiers'.
2005-10-29, by urbanc
1) have adjusted the swapping of the result type
2005-10-29, by urbanc
tuned;
2005-10-28, by wenzelm
lthms_containing: not o valid_thms;
2005-10-28, by wenzelm
added fact_tac, some_fact_tac;
2005-10-28, by wenzelm
renamed Goal constant to prop, more general protect/unprotect interfaces;
2005-10-28, by wenzelm
renamed Goal constant to prop, more general protect/unprotect interfaces;
2005-10-28, by wenzelm
added fact method;
2005-10-28, by wenzelm
tuned ProofContext.export interfaces;
2005-10-28, by wenzelm
syntax for literal facts;
2005-10-28, by wenzelm
removed try_dest_Goal, use Logic.unprotect;
2005-10-28, by wenzelm
added cgoal_of;
2005-10-28, by wenzelm
accomodate simplified Thm.lift_rule;
2005-10-28, by wenzelm
export cong_modifiers, simp_modifiers';
2005-10-28, by wenzelm
certify_term: tuned monomorphic consts;
2005-10-28, by wenzelm
datatype thmref: added Fact;
2005-10-28, by wenzelm
Logic.lift_all;
2005-10-28, by wenzelm
renamed Goal constant to prop, more general protect/unprotect interfaces;
2005-10-28, by wenzelm
renamed Goal.norm_hhf_rule to Goal.norm_hhf;
2005-10-28, by wenzelm
renamed Goal constant to prop, more general protect/unprotect interfaces;
2005-10-28, by wenzelm
added add_local/add_global;
2005-10-28, by wenzelm
added incr_indexes;
2005-10-28, by wenzelm
renamed Goal constant to prop;
2005-10-28, by wenzelm
accomodate simplified Thm.lift_rule;
2005-10-28, by wenzelm
Logic.unprotect;
2005-10-28, by wenzelm
literal facts;
2005-10-28, by wenzelm
* Pure/Isar: literal facts;
2005-10-28, by wenzelm
tuned;
2005-10-28, by wenzelm
unnecessary imports removed
2005-10-28, by webertj
fixed case names in the weak induction principle and
2005-10-28, by urbanc
Implemented proof of weak induction theorem.
2005-10-28, by berghofe
Added "deepen" method.
2005-10-28, by berghofe
circumvented smlnj value restriction
2005-10-28, by haftmann
added extraction interface for code generator
2005-10-28, by haftmann
Added (optional) arguments to the tactics
2005-10-28, by urbanc
cleaned up nth, nth_update, nth_map and nth_string functions
2005-10-28, by haftmann
Removed legacy prove_goalw_cterm command.
2005-10-28, by berghofe
got rid of obsolete prove_goalw_cterm
2005-10-28, by paulson
swapped add_datatype result
2005-10-28, by haftmann
removed obfuscating PStrStrTab
2005-10-28, by haftmann
reachable - abandoned foldl_map in favor of fold_map
2005-10-28, by haftmann
Added Tools/res_hol_clause.ML
2005-10-28, by mengj
Added a new file res_hol_clause.ML to Reconstruction.thy. This file is used to translate HOL formulae into FOL clauses.
2005-10-28, by mengj
Added "writeln_strs" to the signature
2005-10-28, by mengj
Added several new functions that are used to prove HOL goals. Added new methods "vampireH" and "eproverH" that can prove both FOL and HOL goals. The old "vampire" and "eprover" methods are renamed to "vampireF" and "eproverF"; they can only prove FOL goals.
2005-10-28, by mengj
Added new functions to handle HOL goals and lemmas.
2005-10-28, by mengj
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
2005-10-28, by mengj
Added several functions to the signature.
2005-10-28, by mengj
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
2005-10-28, by mengj
sorted lemma lists
2005-10-27, by paulson
* HOL: alternative iff syntax;
2005-10-27, by wenzelm
consts: monomorphic;
2005-10-27, by wenzelm
removed inappropriate monomorphic test;
2005-10-27, by wenzelm
replaced Defs.monomorphic by Sign.monomorphic;
2005-10-27, by wenzelm
alternative iff syntax for equality on booleans, with print_mode 'iff';
2005-10-27, by wenzelm
added module Pure/General/rat.ML
2005-10-27, by haftmann
tidied away duplicate thm
2005-10-26, by paulson
EVERY;
2005-10-25, by wenzelm
traceIt: plain term;
2005-10-25, by wenzelm
val legacy = ref false;
2005-10-25, by wenzelm
prove_raw: cterms, explicit asms;
2005-10-25, by wenzelm
avoid legacy goals;
2005-10-25, by wenzelm
legacy = ref true for the time being -- avoid volumious warnings;
2005-10-22, by wenzelm
tuned;
2005-10-21, by wenzelm
avoid OldGoals shortcuts;
2005-10-21, by wenzelm
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
2005-10-21, by wenzelm
Internal goals.
2005-10-21, by wenzelm
renamed triv_goal to goalI, rev_triv_goal to goalD;
2005-10-21, by wenzelm
tuned header;
2005-10-21, by wenzelm
Goal.norm_hhf_rule;
2005-10-21, by wenzelm
export add_binds_i;
2005-10-21, by wenzelm
load_file: setmp OldGoals.legacy true;
2005-10-21, by wenzelm
improved check_result;
2005-10-21, by wenzelm
Goal.prove_plain;
2005-10-21, by wenzelm
do not export find_thms;
2005-10-21, by wenzelm
use obsolete goals.ML here;
2005-10-21, by wenzelm
Goal.conclude;
2005-10-21, by wenzelm
moved SELECT_GOAL to goal.ML;
2005-10-21, by wenzelm
moved norm_hhf_rule, prove etc. to goal.ML;
2005-10-21, by wenzelm
added simplification tactics and rules (from meta_simplifier.ML);
2005-10-21, by wenzelm
moved various simplification tactics and rules to simplifier.ML;
2005-10-21, by wenzelm
warn_obsolete for goal commands -- danger of disrupting a local proof context;
2005-10-21, by wenzelm
renamed triv_goal to goalI, rev_triv_goal to goalD;
2005-10-21, by wenzelm
added goal.ML;
2005-10-21, by wenzelm
added goal.ML;
2005-10-21, by wenzelm
Goal.norm_hhf_rule, Goal.init;
2005-10-21, by wenzelm
avoid triv_goal and home-grown meta_allE;
2005-10-21, by wenzelm
OldGoals;
2005-10-21, by wenzelm
proper header;
2005-10-21, by wenzelm
avoid home-grown meta_allE;
2005-10-21, by wenzelm
Goal.prove;
2005-10-21, by wenzelm
avoid shortcuts from OldGoals;
2005-10-21, by wenzelm
added simplified settings for Poly/ML 4.x (commented out);
2005-10-21, by wenzelm
reverted (accidental?) change of 1.148;
2005-10-21, by wenzelm
abandoned rational number functions in favor of General/rat.ML
2005-10-21, by haftmann
introduced functions from Pure/General/rat.ML
2005-10-21, by haftmann
slight corrections
2005-10-21, by haftmann
substantially improved integration of website into distribution framework
2005-10-21, by haftmann
substantially improved integration of website into distribution framework
2005-10-21, by haftmann
substantially improved integration of website into distribution framework
2005-10-21, by haftmann
substantially improved integration of website into distribution framework
2005-10-21, by haftmann
towards an improved website/makedist integration
2005-10-21, by haftmann
towards an improved website/makedist integration
2005-10-21, by haftmann
added default distinfo.mak
2005-10-21, by haftmann
towards an improved website/makedist integration
2005-10-21, by haftmann
towards an improved website/makedist integration
2005-10-21, by haftmann
added rounding functions
2005-10-21, by haftmann
Merged theory ResAtpOracle.thy into ResAtpMethods.thy
2005-10-21, by mengj
obsolete;
2005-10-19, by wenzelm
removed add_inductive_x;
2005-10-19, by wenzelm
removed obsolete add_datatype_x;
2005-10-19, by wenzelm
removed obsolete thy_syntax.ML;
2005-10-19, by wenzelm
removed obsolete old_symbol_source;
2005-10-19, by wenzelm
removed obsolete non-Isar theory format and old Isar theory headers;
2005-10-19, by wenzelm
removed old-style theory format;
2005-10-19, by wenzelm
avoid lagacy read function;
2005-10-19, by wenzelm
added thm(s) retrieval functions (from goals.ML);
2005-10-19, by wenzelm
removed obsolete old-locales;
2005-10-19, by wenzelm
removed obsolete axclass_tac, add_inst_subclass_x, add_inst_arity_x;
2005-10-19, by wenzelm
removed obsolete Thy/thy_parse.ML, Thy/thy_scan.ML, Thy/thy_syn.ML;
2005-10-19, by wenzelm
removed obsolete old-style syntax;
2005-10-19, by wenzelm
removed obsolete IOA/meta_theory/ioa_package.ML;
2005-10-19, by wenzelm
removed obsolete domain/interface.ML, IOA/meta_theory/ioa_package.ML;
2005-10-19, by wenzelm
removed obsolete domain/interface.ML;
2005-10-19, by wenzelm
removed obsolete add_typedef_x;
2005-10-19, by wenzelm
removed print_exn (better let the toplevel do this);
2005-10-19, by wenzelm
removed obsolete add_recdef_old;
2005-10-19, by wenzelm
removed obsolete HOL/thy_syntax.ML;
2005-10-19, by wenzelm
* Theory syntax: discontinued non-Isar format and old Isar headers;
2005-10-19, by wenzelm
replaced commafy by existing commas;
2005-10-19, by wenzelm
updated;
2005-10-19, by wenzelm
isatool fixheaders;
2005-10-19, by wenzelm
fix headers;
2005-10-19, by wenzelm
added table functor instance for pairs of strings
2005-10-19, by haftmann
added subgraph
2005-10-19, by haftmann
added join
2005-10-19, by haftmann
slight improvements for website
2005-10-19, by haftmann
moved VAMPIRE_HOME, E_HOME to section "External reasoning tools" -- commented out by default!
2005-10-19, by wenzelm
More functions are added to the signature of ResClause
2005-10-19, by mengj
*** empty log message ***
2005-10-19, by mengj
added 2 lemmas
2005-10-19, by nipkow
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
2005-10-19, by mengj
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
2005-10-18, by wenzelm
tuned error msg;
2005-10-18, by wenzelm
renamed atomize_rule to atomize_cterm;
2005-10-18, by wenzelm
ObjectLogic.atomize_cterm;
2005-10-18, by wenzelm
use simplified Toplevel.proof etc.;
2005-10-18, by wenzelm
back: Toplevel.actual/skip_proof;
2005-10-18, by wenzelm
renamed set_context to context;
2005-10-18, by wenzelm
renamed set_context to context;
2005-10-18, by wenzelm
functor: no Simplifier argument;
2005-10-18, by wenzelm
moved helper lemma to HilbertChoice.thy;
2005-10-18, by wenzelm
Simplifier.theory_context;
2005-10-18, by wenzelm
added lemma exE_some (from specification_package.ML);
2005-10-18, by wenzelm
Simplifier.theory_context;
2005-10-18, by wenzelm
tuned error msg;
2005-10-18, by wenzelm
Simplifier.context/theory_context;
2005-10-18, by wenzelm
updated;
2005-10-18, by wenzelm
new interface to make_conjecture_clauses
2005-10-18, by paulson
* Simplifier: simpset of a running simplification process contains a proof context;
2005-10-17, by wenzelm
added type_solver (uses Simplifier.the_context);
2005-10-17, by wenzelm
added pos/negDivAlg_induct declarations (from Main.thy);
2005-10-17, by wenzelm
moved pos/negDivAlg_induct declarations to Integ/IntDiv.thy;
2005-10-17, by wenzelm
removed obsolete/experimental context components (superceded by Simplifier.the_context);
2005-10-17, by wenzelm
added set/addloop' for simpset dependent loopers;
2005-10-17, by wenzelm
functor: no Simplifier argument;
2005-10-17, by wenzelm
change_claset(_of): more abtract interface;
2005-10-17, by wenzelm
functor: no Simplifier argument;
2005-10-17, by wenzelm
tuned;
2005-10-17, by wenzelm
Simplifier.inherit_context instead of Simplifier.inherit_bounds;
2005-10-17, by wenzelm
change_claset/simpset;
2005-10-17, by wenzelm
change_claset/simpset;
2005-10-17, by wenzelm
Improved proof of injectivity theorems to make it work on
2005-10-17, by berghofe
Fixed bug in proof of support theorem (it failed on constructors with no arguments).
2005-10-17, by berghofe
Implemented proofs for support and freshness theorems.
2005-10-17, by berghofe
deleted leading space in the definition of fresh
2005-10-17, by urbanc
Initial revision.
2005-10-17, by berghofe
tuned;
2005-10-15, by wenzelm
tuned comment;
2005-10-15, by wenzelm
added ML_type, ML_struct;
2005-10-15, by wenzelm
more;
2005-10-15, by wenzelm
* antiquotations ML_type, ML_struct;
2005-10-15, by wenzelm
added guess;
2005-10-15, by wenzelm
added antiquotations ML_type, ML_struct;
2005-10-15, by wenzelm
use perl for test/stat;
2005-10-15, by wenzelm
export strip_params;
2005-10-15, by wenzelm
note_thmss, read/cert_vars etc.: natural argument order;
2005-10-15, by wenzelm
goal statements: before_qed argument;
2005-10-15, by wenzelm
added 'guess', which derives the obtained context from the course of reasoning;
2005-10-15, by wenzelm
added primitive_text, succeed_text;
2005-10-15, by wenzelm
goal statements: accomodate before_qed argument;
2005-10-15, by wenzelm
goal statements: accomodate before_qed argument;
2005-10-15, by wenzelm
added 'guess';
2005-10-15, by wenzelm
tuned;
2005-10-15, by wenzelm
added no_facts;
2005-10-15, by wenzelm
tuned comments;
2005-10-15, by wenzelm
updated;
2005-10-15, by wenzelm
signature changes
2005-10-14, by paulson
added module rat.ML for rational numbers
2005-10-14, by haftmann
longer time out for test (kleing)
2005-10-14, by isatest
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
2005-10-14, by paulson
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
2005-10-14, by paulson
obsolete;
2005-10-13, by wenzelm
counter added to SAT signature
2005-10-12, by webertj
no proof reconstruction when quick_and_dirty is set
2005-10-12, by webertj
tidying
2005-10-12, by paulson
domain package generates compactness lemmas for new constructors
2005-10-12, by huffman
add ML bindings for compactness lemmas
2005-10-12, by huffman
added compactness theorems
2005-10-12, by huffman
added compactness lemmas; cleaned up
2005-10-12, by huffman
added compactness theorems in locale iso
2005-10-11, by huffman
added several theorems in locale iso
2005-10-11, by huffman
added xsymbols syntax for pairs; cleaned up
2005-10-11, by huffman
added theorem typedef_compact
2005-10-11, by huffman
rearranged subsections; added theorems expand_cfun_eq, expand_cfun_less
2005-10-11, by huffman
cleaned up; renamed less_fun to expand_fun_less
2005-10-11, by huffman
added hd lemma
2005-10-11, by nipkow
simplifying the treatment of clausification
2005-10-11, by paulson
simplifying the treatment of nameless theorems
2005-10-11, by paulson
expand: error on undefined/empty env variable;
2005-10-11, by wenzelm
added assert;
2005-10-11, by wenzelm
tuned;
2005-10-11, by wenzelm
added string_of_pid;
2005-10-11, by wenzelm
raw symbols: allow non-ASCII chars (e.g. UTF-8);
2005-10-11, by wenzelm
moved string_of_pid to ML-Systems;
2005-10-11, by wenzelm
ML_SUFFIX in targets (experimental);
2005-10-11, by wenzelm
cleanup backup images;
2005-10-11, by wenzelm
small tidy-up of utility functions
2005-10-10, by paulson
updated print_tac;
2005-10-10, by wenzelm
add names to infix declarations
2005-10-10, by huffman
new syntax translations for continuous lambda abstraction
2005-10-10, by huffman
removed Istrictify; simplified some proofs
2005-10-10, by huffman
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
2005-10-10, by huffman
cleaned up
2005-10-10, by huffman
added theorem typedef_chfin
2005-10-10, by huffman
replaced foldr' with foldr1
2005-10-10, by huffman
cleaned up; renamed "Porder.op <<" to "Porder.<<"
2005-10-10, by huffman
Tactics sat and satx reimplemented, several improvements
2005-10-09, by webertj
tuned Memory.hilim;
2005-10-08, by wenzelm
get rid of feeder -- at the cost of batch-only commit-at-exit;
2005-10-08, by wenzelm
*** empty log message ***
2005-10-08, by nipkow
-nort option;
2005-10-08, by wenzelm
added could_unify;
2005-10-08, by wenzelm
more efficient check_specified, much less invocations;
2005-10-08, by wenzelm
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
2005-10-08, by wenzelm
uses susp.ML, lazy_seq.ML, lazy_scan.ML;
2005-10-08, by wenzelm
added Import/susp.ML, Import/lazy_seq.ML, Import/lasy_scan.ML;
2005-10-08, by wenzelm
minor tweaks for Poplog/PML;
2005-10-08, by wenzelm
tuned memory limits;
2005-10-08, by wenzelm
Int.max;
2005-10-08, by wenzelm
minor tweaks for Poplog/PML;
2005-10-08, by wenzelm
minor tweaks for Poplog/PML;
2005-10-08, by wenzelm
initial pop11 code for ML use/use_string;
2005-10-08, by wenzelm
Poplog/PML: ML_SUFFIX=.psv;
2005-10-08, by wenzelm
support ML_SUFFIX;
2005-10-08, by wenzelm
obsolete;
2005-10-08, by wenzelm
fix due to new neq_simproc
2005-10-08, by nipkow
removed obsolete comment;
2005-10-07, by wenzelm
added idtypdummy_ast_tr;
2005-10-07, by wenzelm
added syntax for _idtdummy, _idtypdummy;
2005-10-07, by wenzelm
added absdummy;
2005-10-07, by wenzelm
removed obsolete dummy_pat_tr;
2005-10-07, by wenzelm
Term.absdummy;
2005-10-07, by wenzelm
removed obsolete ex/Tuple.thy;
2005-10-07, by wenzelm
replaced _K by dummy abstraction;
2005-10-07, by wenzelm
print_translation: does not handle _idtdummy;
2005-10-07, by wenzelm
tuned;
2005-10-07, by wenzelm
added dummy variable binding;
2005-10-07, by wenzelm
changes due to new neq_simproc in simpdata.ML
2005-10-07, by nipkow
added str_of_term (from HOL/Tools/ATP/recon_translate_proof.ML);
2005-10-07, by wenzelm
Term.str_of_term;
2005-10-07, by wenzelm
minor code tidyig
2005-10-07, by paulson
code restructuring
2005-10-07, by paulson
more tidying. Fixed process management bugs and race condition
2005-10-07, by paulson
major simplification: removal of the goalstring argument
2005-10-06, by paulson
Optimized getPreds and getSuccs.
2005-10-06, by berghofe
adjusted sydney to new website
2005-10-06, by haftmann
changed sydney share
2005-10-06, by haftmann
added Poplog/PML version 15.6/2.1 (experimental!);
2005-10-05, by wenzelm
added fold_nodes, map_node_yield
2005-10-05, by haftmann
added merge, tuned
2005-10-05, by haftmann
added last in set lemma
2005-10-05, by nipkow
improved process handling. tidied
2005-10-05, by paulson
more signals
2005-10-05, by paulson
new hd/rev/last lemmas
2005-10-04, by nipkow
new lemmas
2005-10-04, by nipkow
added compiler and runtime options;
2005-10-04, by wenzelm
Poplog/PML startup script.
2005-10-04, by wenzelm
Compatibility file for Poplog/PML (version 15.6/2.1).
2005-10-04, by wenzelm
Substring.all = Substring.full;
2005-10-04, by wenzelm
minor tweaks for Poplog/ML;
2005-10-04, by wenzelm
find_theorems: support * wildcard in name: criterion;
2005-10-04, by wenzelm
* Command 'find_theorems': support * wildcard in name: criterion.
2005-10-04, by wenzelm
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit this into ML_dbase!
2005-10-04, by wenzelm
added redirect.html
2005-10-04, by haftmann
better error handling
2005-10-04, by haftmann
improved linktest
2005-10-04, by haftmann
removed removed IntFloor
2005-10-04, by haftmann
fixed broken link
2005-10-04, by haftmann
fixed broken mailto: link
2005-10-04, by haftmann
fixed the ascii-armouring of goalstring
2005-10-04, by paulson
reset clause counter
2005-10-04, by paulson
theorems need names
2005-10-04, by paulson
support for setting local permissions
2005-10-04, by haftmann
improved dependency build
2005-10-04, by haftmann
added conf/ to .cvsignore
2005-10-04, by haftmann
Add icon for interface.
Isabelle2005
2005-09-30, by aspinall
Move welcomemsg and helpdoc to pgip_isar.xml
2005-09-30, by aspinall
Add helpdocs and welcomemsg here instead of hard wiring in proof_general.ML.
2005-09-30, by aspinall
Explanatory text
2005-09-30, by aspinall
Schema files (for information, and validating pgip_isar.xml)
2005-09-30, by aspinall
Schema for PGIP
2005-09-30, by aspinall
pruned notes about Poly/ML;
2005-09-30, by wenzelm
converted to Isar theory format;
2005-09-30, by wenzelm
Initialise pgip id also for Emacs mode. Allow dynamic config file location for PGIP.
2005-09-30, by aspinall
tuned;
2005-09-30, by wenzelm
Fix for guiconfig -> displayconfig element rename
2005-09-30, by aspinall
theorems need names
2005-09-30, by paulson
refer to $PRG instead of (old) rsync-isabelle;
2005-09-29, by wenzelm
updated;
2005-09-29, by wenzelm
updated;
2005-09-29, by wenzelm
pdfsetup.sty: better not rely on ifpdf.sty;
2005-09-29, by wenzelm
simprules need names
2005-09-29, by paulson
export debug_bounds;
2005-09-29, by wenzelm
explicit dependencies of SAT vs. Refute;
2005-09-29, by wenzelm
explicit dependencies of SAT vs. Refute;
2005-09-29, by wenzelm
Isabelle2005 (October 2005);
2005-09-29, by wenzelm
Added a few lemmas
2005-09-29, by nipkow
reduction in tracing files
2005-09-29, by paulson
improvements for problem generation
2005-09-29, by paulson
moved concat_with_and to watcher.ML
2005-09-29, by paulson
a name for empty_not_insert
2005-09-29, by paulson
Simplifier now removes flex-flex constraints from theorem returned by prover.
2005-09-29, by berghofe
Optimized and exported flexflex_unique.
2005-09-29, by berghofe
make signature constraint actually work;
2005-09-29, by wenzelm
activate signature constraints;
2005-09-29, by wenzelm
HOL4 image is back;
2005-09-29, by wenzelm
tuned default operation: use internal modify;
2005-09-29, by wenzelm
abstract_rule: tuned exception msgs;
2005-09-29, by wenzelm
back to simple 'defs' (cf. revision 1.79 of theory.ML);
2005-09-29, by wenzelm
back to simple 'defs' (cf. revision 1.79);
2005-09-29, by wenzelm
removed revert_bound;
2005-09-29, by wenzelm
print_theory: discontinued final consts;
2005-09-29, by wenzelm
Theory.add_finals_i;
2005-09-29, by wenzelm
more finalconsts;
2005-09-29, by wenzelm
tuned;
2005-09-29, by wenzelm
pointer to HOL/ex/SAT_Examples.thy added
2005-09-28, by webertj
updated;
2005-09-28, by wenzelm
more reliable check for PDF output using ifpdf.sty;
2005-09-28, by wenzelm
pre_sat_tac moved towards end of file
2005-09-28, by webertj
adjusted www links
2005-09-28, by haftmann
comment fixed
2005-09-28, by webertj
mapped "-->" to "hol4-->"
2005-09-28, by obua
avoid naming existing tags in explanations;
2005-09-28, by wenzelm
revert 'defs' advertisement;
2005-09-28, by wenzelm
revert 'defs' advertisement;
2005-09-28, by wenzelm
time limit option; fixed bug concerning first line of ATP output
2005-09-28, by paulson
streamlined theory; conformance to recent publication
2005-09-28, by paulson
new lemma
2005-09-28, by paulson
better appearance in lynx and netscape4
2005-09-28, by haftmann
MB instead of KB
2005-09-28, by haftmann
renamed packages to download;
2005-09-27, by wenzelm
more details about incomplete 'defs';
2005-09-27, by wenzelm
renamed "Packages" to "Download";
2005-09-27, by wenzelm
build bed
2005-09-27, by haftmann
build bed
2005-09-27, by haftmann
build bed
2005-09-27, by haftmann
slight corrections
2005-09-27, by haftmann
tuned;
2005-09-27, by wenzelm
renamed "Packages" to "Download";
2005-09-27, by wenzelm
fixed dead link
2005-09-27, by haftmann
fixed dead link
2005-09-27, by haftmann
improved linkcheck
2005-09-27, by haftmann
added simple linktester for isabelle website
2005-09-27, by haftmann
warn about Poly/ML segfault problem;
2005-09-27, by wenzelm
website preparation for Isabelle2005
2005-09-27, by haftmann
corrected spelling bug
2005-09-27, by obua
added defs disclaimer
2005-09-27, by obua
nat_number_of is no longer declared as code lemma, since this turned
2005-09-27, by berghofe
Inserted clause for nat in number_of_codegen again ("code unfold" turned
2005-09-27, by berghofe
Optimized unfold_attr.
2005-09-27, by berghofe
removed link to HOL4, which is not in the library right now;
2005-09-27, by wenzelm
tuned;
2005-09-27, by wenzelm
Added entries for code_module, code_library, and value.
2005-09-27, by berghofe
Tuned.
2005-09-27, by berghofe
updates for Isabelle2005;
2005-09-26, by wenzelm
tuned;
2005-09-26, by wenzelm
Updated description of code generator.
2005-09-26, by berghofe
updated;
2005-09-26, by wenzelm
moved disambiguate_frees to ProofKernel;
2005-09-26, by wenzelm
quote 'value';
2005-09-26, by wenzelm
yet another atempt to get doc/Contents right;
2005-09-26, by wenzelm
Renamed wf_rec to wfrec in consts_code declaration.
2005-09-26, by berghofe
really copy doc/Contents;
2005-09-26, by wenzelm
Release HOL4 and HOLLight Importer.
2005-09-26, by obua
copy doc/Contents;
2005-09-26, by wenzelm
Made sure all lemmas now have names (especially so that certain of them
2005-09-26, by skalberg
echo HOL_USERDIR_OPTIONS;
2005-09-26, by wenzelm
tuned
2005-09-26, by obua
added ROOT.ML
2005-09-26, by obua
adjusted web link
2005-09-26, by haftmann
added entry for running HOLLight
2005-09-26, by obua
fixed disambiguation problem
2005-09-26, by obua
added Drule.disambiguate_frees : thm -> thm
2005-09-26, by obua
zero_var_inst: replace loose bounds :000 etc.;
2005-09-25, by wenzelm
* Hyperreal: A theory of Taylor series.
2005-09-25, by wenzelm
more;
2005-09-25, by wenzelm
eq_codegen now ensures that code for bool type is generated.
2005-09-25, by berghofe
Fixed print mode problem in test_term.
2005-09-25, by berghofe
Added ExecutableSet and Taylor.
2005-09-25, by berghofe
Now uses set implementation from ExecutableSet.
2005-09-25, by berghofe
Added Taylor.
2005-09-25, by berghofe
Formalization of Taylor series by Lukas Bulwahn and
2005-09-25, by berghofe
Added ExecutableSet.
2005-09-25, by berghofe
New theory for implementing finite sets by lists.
2005-09-25, by berghofe
sat_solver.ML not loaded anymore (already loaded by Refute.thy)
2005-09-25, by webertj
set show_types and show_sorts during import
2005-09-24, by obua
a few new filter lemmas
2005-09-24, by nipkow
HOL4-Import: map ONTO to Fun.surj
2005-09-24, by obua
cnf_struct renamed to cnf
2005-09-24, by webertj
remove debug clutter
2005-09-24, by obua
preliminary fix of HOL build problem
2005-09-24, by obua
bug fix
2005-09-24, by obua
replay_proof optimized: now performs backwards proof search
2005-09-24, by webertj
code reformatted and restructured, many minor modifications
2005-09-24, by webertj
bugfix in "zchaff_with_proofs"
2005-09-24, by webertj
parse_std_result_file renamed to read_std_result_file
2005-09-24, by webertj
new sat tactic
2005-09-23, by webertj
new sat tactic imports resolution proofs from zChaff
2005-09-23, by webertj
fix
2005-09-23, by obua
simprocs: pattern now "x" (the proc is supposed to discriminate faster than Pattern.match);
2005-09-23, by wenzelm
tuned msg;
2005-09-23, by wenzelm
added mk_solver';
2005-09-23, by wenzelm
Simplifier.inherit_bounds;
2005-09-23, by wenzelm
adm_tac/cont_tacRs: proper simpset;
2005-09-23, by wenzelm
Provers/Arith/fast_lin_arith.ML: Simplifier.inherit_bounds;
2005-09-23, by wenzelm
tuned order of targets;
2005-09-23, by wenzelm
Provers/cancel_sums.ML: Simplifier.inherit_bounds;
2005-09-23, by wenzelm
some typos in comments fixed
2005-09-23, by webertj
1) fixed bug in type_introduction: first stage uses different namespace than second stage
2005-09-23, by obua
removed doc/index.html from distribution (now produced by website);
2005-09-23, by wenzelm
mkdir -p for symlinks
2005-09-23, by haftmann
rules -> iprover
2005-09-23, by nipkow
spaces inserted in header
2005-09-23, by webertj
header (title/ID) added
2005-09-23, by webertj
typo fixed: rufute -> refute
2005-09-23, by webertj
bugfix in record_tr'
2005-09-23, by schirmer
method 'rules' renamed to 'iprover', which does *not* retrieve theorems from the Internet;
2005-09-23, by wenzelm
Id;
2005-09-23, by wenzelm
tuned;
2005-09-23, by wenzelm
changed defaults
2005-09-23, by paulson
ATP linkup
2005-09-23, by paulson
replay type_introduction fix
2005-09-23, by obua
temporarily re-introduced overwrite_warn
2005-09-23, by haftmann
add debug messages
2005-09-23, by obua
renamed rules to iprover
2005-09-23, by nipkow
*** empty log message ***
2005-09-23, by nipkow
renamed rules to iprover
2005-09-22, by nipkow
fix because of list lemmas
2005-09-22, by nipkow
renamed "rules" to "iprover"
2005-09-22, by nipkow
added theorem adm_ball
2005-09-22, by huffman
cleaned up
2005-09-22, by huffman
HOLCF theorem naming conventions
2005-09-22, by huffman
removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
2005-09-22, by paulson
Fix because of new lemma in List
2005-09-22, by nipkow
solver "auto" does not reverse the list of solvers anymore
2005-09-22, by webertj
added fold_map_graph
2005-09-22, by haftmann
added fold_map_table
2005-09-22, by haftmann
only show trunk in Changelog (kleing)
2005-09-22, by isatest
zchaff_with_proofs does not delete zChaff\s resolve_trace file anymore
2005-09-21, by webertj
echo HOL_USEDIR_OPTIONS;
2005-09-21, by wenzelm
tuned;
2005-09-21, by wenzelm
PROOFGENERAL_OPTIONS: smart fall-back on plain emacs (back again);
2005-09-21, by wenzelm
updated for Isabelle2005;
2005-09-21, by wenzelm
tuned;
2005-09-21, by wenzelm
updated for Isabelle2005;
2005-09-21, by wenzelm
less
more
|
(0)
-10000
-3000
-1000
-480
+480
+1000
+3000
+10000
+30000
tip