Mercurial
Mercurial
>
repos
>
testboard
/ 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 JavaScriptenabled browsers.
add type constraint to otherwise looping iff rule
20060917, by huffman
generalize type of (NS)LIM to work on functions with vector space domain types
20060917, by huffman
norm_one is now proved from other class axioms
20060917, by huffman
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
20060917, by huffman
hcmod abbreviates hnorm :: hcomplex => hypreal
20060917, by huffman
complex_of_real abbreviates of_real::real=>complex;
20060916, by huffman
add instance for real_algebra_1 and real_normed_div_algebra
20060916, by huffman
add instances for real_vector and real_algebra
20060916, by huffman
define new constant of_real for class real_algebra_1;
20060916, by huffman
int_diff_cases moved to Integ/IntDef.thy
20060916, by huffman
generalized types of many constants to work over arbitrary vector spaces;
20060916, by huffman
add theorem norm_diff_triangle_ineq
20060916, by huffman
add required type annotation
20060916, by huffman
removed type aliases for theory/theory_ref;
20060915, by wenzelm
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
20060915, by wenzelm
tuned;
20060915, by wenzelm
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
20060915, by wenzelm
instantiate: omit has_duplicates check, which is irrelevant for soundness;
20060915, by wenzelm
trivial whitespace change
20060915, by webertj
tuned;
20060915, by wenzelm
more on theorems;
20060914, by wenzelm
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
20060914, by huffman
add instance for class division_ring
20060914, by huffman
removed duplicate lemmas
20060914, by huffman
fixed syntax clash with Real/RealVector
20060914, by huffman
*** empty log message ***
20060914, by wenzelm
Function package: Outside their domain functions now return "arbitrary".
20060914, by krauss
updated makefile
20060914, by krauss
Fixed Subscript Exception occurring with HigherOrder recursion
20060914, by krauss
remove conflicting norm syntax
20060914, by huffman
made SML/NJ happy;
20060914, by wenzelm
added exists_type;
20060913, by wenzelm
renamed NameSpace.drop_base to NameSpace.qualifier;
20060913, by wenzelm
Updated keyword file
20060913, by krauss
Removed debugging code imports...
20060913, by krauss
Added the "theory_const" option. Only it is OFF because it's often harmful!
20060913, by paulson
Extended the blacklist with higherorder theorems. Restructured. Added checks to
20060913, by paulson
bug fix to abstractions: free variables in theorem can be abstracted over.
20060913, by paulson
Tweaks to is_fol_term, the firstorder test. We don't count "=" as a connective
20060913, by paulson
Major update to function package, including new syntax and the (only theoretical)
20060913, by krauss
added instance rat :: recpower
20060913, by huffman
more on theorems;
20060912, by wenzelm
tuned;
20060912, by wenzelm
more on terms;
20060912, by wenzelm
no_syntax norm  clash with Real/RealVector.thy;
20060912, by wenzelm
simplify some proofs, remove obsolete realpow_divide
20060912, by huffman
realpow_divide > power_divide
20060912, by huffman
remove extra dependency
20060912, by huffman
more on terms;
20060912, by wenzelm
Efficient term substitution  avoids copying.
20060912, by wenzelm
ctyp: maintain maxidx;
20060912, by wenzelm
removed obsolete aconvs (use eq_list aconv);
20060912, by wenzelm
tuned eq_list;
20060912, by wenzelm
moved term subst functions to TermSubst;
20060912, by wenzelm
intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
20060912, by wenzelm
added Pure/term_subst.ML;
20060912, by wenzelm
added Gentzen:1935;
20060912, by wenzelm
import RealVector
20060912, by huffman
formalization of vector spaces and algebras over the real numbers
20060912, by huffman
induct method: renamed 'fixing' to 'arbitrary';
20060911, by wenzelm
less
more

(0)
10000
3000
1000
300
100
60
+60
+100
+300
+1000
+3000
+10000
+30000
tip