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 JavaScriptenabled browsers.
add Real/RealVector.thy
20060919, by huffman
* Pure: 'class_deps' command visualizes the subclass relation;
20060918, by wenzelm
added class_deps;
20060918, by wenzelm
added dest_arg, i.e. a tuned version of #2 o dest_comb;
20060918, by wenzelm
Thm.dest_arg;
20060918, by wenzelm
Present.display_graph;
20060918, by wenzelm
added display_graph (from thm_deps.ML);
20060918, by wenzelm
output: uninterpreted raw symbols  these are usually LaTeX macros;
20060918, by wenzelm
pretty_thm: graceful treatment of ProtoPure.thy;
20060918, by wenzelm
added class_deps;
20060918, by wenzelm
classes: maintain serial number;
20060918, by wenzelm
tuned;
20060918, by wenzelm
isatool browser: renamed option d to c (cf. isatool tool)
20060918, by wenzelm
PRIVATE_FILE: slightly more robust way to create and dispose;
20060918, by wenzelm
renamed option d to c (cf. isatool display);
20060918, by wenzelm
updated;
20060918, by wenzelm
Bug fix to prevent exception dest_Free from escaping
20060918, by paulson
Added the max_new parameter, which is a cap on how many clauses may be admitted per round.
20060918, by paulson
replaced implodeable_Ext by set_like
20060918, 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)
20060918, by chaieb
replace (x +  y) with (x  y)
20060918, by huffman
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
less
more

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