Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+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.
updated;
2006-09-18, by wenzelm
Bug fix to prevent exception dest_Free from escaping
2006-09-18, by paulson
Added the max_new parameter, which is a cap on how many clauses may be admitted per round.
2006-09-18, by paulson
replaced implodeable_Ext by set_like
2006-09-18, by obua
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
2006-09-18, by chaieb
replace (x + - y) with (x - y)
2006-09-18, by huffman
add type constraint to otherwise looping iff rule
2006-09-17, by huffman
generalize type of (NS)LIM to work on functions with vector space domain types
2006-09-17, by huffman
norm_one is now proved from other class axioms
2006-09-17, by huffman
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
2006-09-17, by huffman
hcmod abbreviates hnorm :: hcomplex => hypreal
2006-09-17, by huffman
complex_of_real abbreviates of_real::real=>complex;
2006-09-16, by huffman
add instance for real_algebra_1 and real_normed_div_algebra
2006-09-16, by huffman
add instances for real_vector and real_algebra
2006-09-16, by huffman
define new constant of_real for class real_algebra_1;
2006-09-16, by huffman
int_diff_cases moved to Integ/IntDef.thy
2006-09-16, by huffman
generalized types of many constants to work over arbitrary vector spaces;
2006-09-16, by huffman
add theorem norm_diff_triangle_ineq
2006-09-16, by huffman
add required type annotation
2006-09-16, by huffman
removed type aliases for theory/theory_ref;
2006-09-15, by wenzelm
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
2006-09-15, by wenzelm
tuned;
2006-09-15, by wenzelm
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
2006-09-15, by wenzelm
instantiate: omit has_duplicates check, which is irrelevant for soundness;
2006-09-15, by wenzelm
trivial whitespace change
2006-09-15, by webertj
tuned;
2006-09-15, by wenzelm
more on theorems;
2006-09-14, by wenzelm
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
2006-09-14, by huffman
add instance for class division_ring
2006-09-14, by huffman
removed duplicate lemmas
2006-09-14, by huffman
fixed syntax clash with Real/RealVector
2006-09-14, by huffman
*** empty log message ***
2006-09-14, by wenzelm
Function package: Outside their domain functions now return "arbitrary".
2006-09-14, by krauss
updated makefile
2006-09-14, by krauss
Fixed Subscript Exception occurring with Higher-Order recursion
2006-09-14, by krauss
remove conflicting norm syntax
2006-09-14, by huffman
made SML/NJ happy;
2006-09-14, by wenzelm
added exists_type;
2006-09-13, by wenzelm
renamed NameSpace.drop_base to NameSpace.qualifier;
2006-09-13, by wenzelm
Updated keyword file
2006-09-13, by krauss
Removed debugging code imports...
2006-09-13, by krauss
Added the "theory_const" option. Only it is OFF because it's often harmful!
2006-09-13, by paulson
Extended the blacklist with higher-order theorems. Restructured. Added checks to
2006-09-13, by paulson
bug fix to abstractions: free variables in theorem can be abstracted over.
2006-09-13, by paulson
Tweaks to is_fol_term, the first-order test. We don't count "=" as a connective
2006-09-13, by paulson
Major update to function package, including new syntax and the (only theoretical)
2006-09-13, by krauss
added instance rat :: recpower
2006-09-13, by huffman
more on theorems;
2006-09-12, by wenzelm
tuned;
2006-09-12, by wenzelm
more on terms;
2006-09-12, by wenzelm
no_syntax norm -- clash with Real/RealVector.thy;
2006-09-12, by wenzelm
simplify some proofs, remove obsolete realpow_divide
2006-09-12, by huffman
realpow_divide -> power_divide
2006-09-12, by huffman
remove extra dependency
2006-09-12, by huffman
more on terms;
2006-09-12, by wenzelm
Efficient term substitution -- avoids copying.
2006-09-12, by wenzelm
ctyp: maintain maxidx;
2006-09-12, by wenzelm
removed obsolete aconvs (use eq_list aconv);
2006-09-12, by wenzelm
tuned eq_list;
2006-09-12, by wenzelm
moved term subst functions to TermSubst;
2006-09-12, by wenzelm
less
more
|
(0)
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip