Mercurial
Mercurial
>
repos
>
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
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.
refinements
2006-08-29, by haftmann
added and refined some exmples
2006-08-29, by haftmann
added typecopy_package
2006-08-29, by haftmann
added typecopy_package and some examples
2006-08-29, by haftmann
updated keywords
2006-08-29, by haftmann
minor bug fixes
2006-08-28, by paulson
removed the (apparently pointless) signature constraint
2006-08-28, by paulson
tidied
2006-08-28, by paulson
encode clauses as Isar premises, rather than as object-logic &, for faster parsing
2006-08-28, by webertj
abstraction of lambda-expressions
2006-08-25, by paulson
tidied
2006-08-25, by paulson
better skolemization, using first-order resolution rather than hoping for the right result
2006-08-25, by paulson
using inc
2006-08-25, by paulson
explicit type variables prevent empty sorts
2006-08-25, by paulson
replaced skolem declarations by automatic skolemization of everything
2006-08-25, by paulson
avoid duplicate tactics
2006-08-25, by webertj
additional list of tactics that can be added to arith
2006-08-24, by webertj
Added premises concerning finite support of recursion results to FCBs.
2006-08-24, by berghofe
speed up proof of summable_Cauchy
2006-08-23, by huffman
speed up some proofs
2006-08-23, by huffman
generalize proof of SUP_rabs_subseq
2006-08-23, by huffman
speed up some proofs
2006-08-23, by huffman
SML/NJ int type fix
2006-08-23, by haftmann
tracing
2006-08-21, by haftmann
improved preprocessing
2006-08-21, by haftmann
fixed bug in sortlookup
2006-08-21, by haftmann
more concise preprocessing of numerals for code generation
2006-08-21, by haftmann
more concise string serialization
2006-08-21, by haftmann
added some codegen examples/applications
2006-08-21, by haftmann
adapted using the characteristic equations
2006-08-18, by urbanc
modified to use the characteristic equations
2006-08-18, by urbanc
- Fixed bug that caused uniqueness proof for recursion
2006-08-18, by berghofe
used the recursion combinator for the height and substitution function
2006-08-17, by urbanc
added definition for size and substitution using the recursion
2006-08-17, by urbanc
improved thmtab
2006-08-17, by haftmann
fixed bug in sortcontext extraction
2006-08-17, by haftmann
dropped definitions_of
2006-08-17, by haftmann
added all_super_classes
2006-08-17, by haftmann
renamed module to thyname
2006-08-17, by haftmann
cleanup
2006-08-17, by haftmann
added missing supp_nat lemma
2006-08-16, by urbanc
added
2006-08-14, by haftmann
module restructuring
2006-08-14, by haftmann
code cleanup, instance_subsort now working
2006-08-14, by haftmann
added code generator packages
2006-08-14, by haftmann
adaptions to improvements
2006-08-14, by haftmann
added add_hook_bootstrap
2006-08-14, by haftmann
added new files
2006-08-14, by haftmann
simplified code generator setup
2006-08-14, by haftmann
added passage on class package
2006-08-14, by haftmann
updated code generator keywords
2006-08-14, by haftmann
Removed non-trivial definitions from calc_atm theorem list.
2006-08-14, by berghofe
Finished implementation of uniqueness proof for recursion combinator.
2006-08-14, by berghofe
*** empty log message ***
2006-08-14, by chaieb
Reification now handels binders.
2006-08-14, by chaieb
consistent prefixing for skolem functions
2006-08-09, by paulson
blacklist augmented to block some "unit" theorems that cause unsound resolution proofs
2006-08-09, by paulson
tuned: string_of_list, string_of_pair
2006-08-09, by webertj
* ProofContext.prems_limit is now -1 by default;
2006-08-09, by wenzelm
tuned proofs;
2006-08-09, by wenzelm
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
2006-08-09, by wenzelm
renamed map_theory to theory;
2006-08-09, by wenzelm
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
2006-08-09, by wenzelm
locale interpretation command: after_qed;
2006-08-09, by wenzelm
int_option: signed_string_of_int;
2006-08-09, by wenzelm
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
2006-08-09, by wenzelm
skolem declarations for built-in theorems
2006-08-08, by paulson
more explict variable names
2006-08-08, by paulson
tidying
2006-08-08, by paulson
Adapted to older logfiles containing no cpu time.
2006-08-08, by berghofe
added code_constname keyword
2006-08-08, by haftmann
fixed code generator theorem generation
2006-08-08, by haftmann
improvements for 2nd codegenerator
2006-08-08, by haftmann
cleanup code generation for Numerals
2006-08-08, by haftmann
improved & fixed code generator theorem generation
2006-08-08, by haftmann
code generator refinements
2006-08-08, by haftmann
adding code lemma now works as expected
2006-08-08, by haftmann
added more examples
2006-08-08, by haftmann
dropped duplicated line
2006-08-08, by haftmann
added Tools/typedef_codegen.ML
2006-08-08, by haftmann
abandoned equal_list in favor for eq_list
2006-08-08, by haftmann
Simple ML script for producing Gnuplot files from
2006-08-07, by berghofe
title fixed
2006-08-07, by webertj
updated;
2006-08-05, by wenzelm
avoid low-level tsig;
2006-08-05, by wenzelm
reworked read_instantiate -- separate read_insts;
2006-08-05, by wenzelm
tuned;
2006-08-05, by wenzelm
removed obsolete sign_of;
2006-08-05, by wenzelm
Amine Chaieb: experimental generic reflection and reification in HOL;
2006-08-05, by wenzelm
use atbroy101 instead of atbroy98 (freezes up)
2006-08-05, by isatest
Added Keywords: "otherwise" and "sequential", needed for function package's
2006-08-04, by krauss
*** empty log message ***
2006-08-04, by chaieb
Rule instantiations -- operations within a rule/subgoal context.
2006-08-03, by wenzelm
moved bires_inst_tac etc. to rule_insts.ML;
2006-08-03, by wenzelm
moved read_instantiate etc. to rule_insts.ML;
2006-08-03, by wenzelm
added Isar/rule_insts.ML;
2006-08-03, by wenzelm
removed obsolete commute, map_list;
2006-08-03, by wenzelm
removed obsolete add_term_tvarnames;
2006-08-03, by wenzelm
tuned;
2006-08-03, by wenzelm
tuned types_sorts, add_used;
2006-08-03, by wenzelm
RuleInsts.bires_inst_tac;
2006-08-03, by wenzelm
*** empty log message ***
2006-08-03, by chaieb
fixed generator
2006-08-03, by obua
added HOL/ex/Reflection;
2006-08-03, by wenzelm
removed True_implies (cf. True_implies_equals);
2006-08-03, by wenzelm
removed OldGoals.legacy flag (always warn);
2006-08-03, by wenzelm
removed OldGoals.legacy flag (always warn);
2006-08-03, by wenzelm
tuned;
2006-08-03, by wenzelm
removed True_implies (cf. True_implies_equals);
2006-08-03, by wenzelm
Generic reflection and reification (by Amine Chaieb).
2006-08-03, by wenzelm
Restructured algebra library, added ideals and quotient rings.
2006-08-03, by ballarin
Updated comments.
2006-08-03, by ballarin
updated;
2006-08-03, by wenzelm
tuned proofs;
2006-08-02, by wenzelm
lemma da_good_approx: adapted induction (was exploting lifted obtain result);
2006-08-02, by wenzelm
renamed Syntax.indexname to Syntax.read_indexname;
2006-08-02, by wenzelm
tuned;
2006-08-02, by wenzelm
moved debug option to proof_display.ML (again);
2006-08-02, by wenzelm
normalized Proof.context/method type aliases;
2006-08-02, by wenzelm
simplified Assumption/ProofContext.export;
2006-08-02, by wenzelm
less
more
|
(0)
-10000
-3000
-1000
-120
+120
+1000
+3000
+10000
+30000
tip