Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-300
-100
-56
+56
+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.
auxiliary dynamic_thm(s) for fact lookup;
2008-03-19, by wenzelm
auxiliary dynamic_thm(s) for fact lookup;
2008-03-19, by wenzelm
renamed datatype thmref to Facts.ref, tuned interfaces;
2008-03-19, by wenzelm
removed redundant Nat.less_not_sym, Nat.less_asym;
2008-03-19, by wenzelm
removed redundant Nat.less_irrefl;
2008-03-19, by wenzelm
Attributes sledgehammer_full, sledgehammer_modulus, sledgehammer_sorts
2008-03-19, by paulson
system: writeln output, if available;
2008-03-19, by wenzelm
error tuning
2008-03-19, by haftmann
moved typ_of_inst to Type.typ_of_sort
2008-03-19, by haftmann
instantiation less liberal with dangling constraints
2008-03-19, by haftmann
Type.lookup now curried
2008-03-19, by haftmann
Type.lookup now curried; typ_of_sort
2008-03-19, by haftmann
new class error case NoSubsort
2008-03-19, by haftmann
quickcheck with term reconstruction
2008-03-19, by haftmann
whitespace tuning
2008-03-19, by haftmann
theory loader: discontinued *attached* ML scripts;
2008-03-18, by wenzelm
converted legacy ML scripts;
2008-03-18, by wenzelm
valid_thms: get_thms_silent;
2008-03-18, by wenzelm
removed check_lookup;
2008-03-18, by wenzelm
added ckeck_lookup flag (default false), which controls sanity check of thm lookup;
2008-03-18, by wenzelm
updated generated files;
2008-03-18, by wenzelm
tuned proof;
2008-03-18, by wenzelm
removed redundant less_trans, less_linear, le_imp_less_or_eq, le_less_trans, less_le_trans (cf. Orderings.thy);
2008-03-18, by wenzelm
removed redundant less_trans, less_linear, le_imp_less_or_eq, le_less_trans, less_le_trans (cf. Orderings.thy);
2008-03-18, by wenzelm
avoid rebinding of existing facts;
2008-03-18, by wenzelm
avoid rebinding of existing facts;
2008-03-17, by wenzelm
avoid rebinding of existing facts;
2008-03-17, by wenzelm
removed duplicate lemmas;
2008-03-17, by wenzelm
only one version of group.rcos_self;
2008-03-17, by wenzelm
Facts.add_local;
2008-03-17, by wenzelm
Facts.add_global;
2008-03-17, by wenzelm
replaced generic add by add_local/add_global;
2008-03-17, by wenzelm
proper naming of weak_ref_map2ref_map;
2008-03-17, by wenzelm
avoid rebinding of existing facts;
2008-03-17, by wenzelm
avoid rebinding of existing facts;
2008-03-17, by wenzelm
added Compl_Collect;
2008-03-17, by wenzelm
proper naming of knows_Outpts_insecureM, knows_subset_knows_A_Gets;
2008-03-17, by wenzelm
renamed K3_imp_Gets variant to K3_imp_Gets_evs;
2008-03-17, by wenzelm
removed duplicate lemmas;
2008-03-17, by wenzelm
closeup: recover original order of free variables!
2008-03-17, by wenzelm
reorganization
2008-03-17, by nipkow
added lemmas
2008-03-17, by nipkow
remove unneeded constant mod_alt
2008-03-17, by huffman
More defns and thms
2008-03-17, by nipkow
fixed broken bintrunc lemma
2008-03-17, by kleing
tuned;
2008-03-15, by wenzelm
get_thm(s): check facts lookup vs. old thm database;
2008-03-15, by wenzelm
tuned messages;
2008-03-15, by wenzelm
del: hide in name space;
2008-03-15, by wenzelm
avoid unclear fact references;
2008-03-15, by wenzelm
eliminated out-of-scope proofs (cf. theory IFOL and FOL);
2008-03-15, by wenzelm
proper antiquotations;
2008-03-15, by wenzelm
added lemmas from simpdata.ML;
2008-03-15, by wenzelm
removed obsolete PureThy.thms_containing;
2008-03-15, by wenzelm
replaced obsolete FactIndex.T by Facts.T;
2008-03-15, by wenzelm
more precise Author line;
2008-03-15, by wenzelm
less
more
|
(0)
-10000
-3000
-1000
-300
-100
-56
+56
+100
+300
+1000
+3000
+10000
+30000
tip