Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-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.
more robust handling of theory context;
1999-02-05, by wenzelm
improved theory, context, update_context;
1999-02-05, by wenzelm
improved 'theory';
1999-02-05, by wenzelm
improved msg;
1999-02-05, by wenzelm
use_thy, update_thy: Context.save;
1999-02-05, by wenzelm
tuned;
1999-02-05, by wenzelm
time_use made pervasive;
1999-02-05, by wenzelm
use_dir: check parent, more robust exit;
1999-02-05, by wenzelm
more robust RC;
1999-02-05, by wenzelm
setmp: theory option;
1999-02-05, by wenzelm
Session.finish ();
1999-02-05, by wenzelm
tidied Schroeder-Bernstein proof
1999-02-05, by paulson
new surj rules
1999-02-05, by paulson
obsolete;
1999-02-04, by wenzelm
tuned;
1999-02-04, by wenzelm
include full paths in file info;
1999-02-04, by wenzelm
Symbol.use;
1999-02-04, by wenzelm
Symbol.use (eliminated Use.exit_use);
1999-02-04, by wenzelm
leave theory context after load_thy;
1999-02-04, by wenzelm
File.pwd, File.cd;
1999-02-04, by wenzelm
fixed file_info;
1999-02-04, by wenzelm
use, cd;
1999-02-04, by wenzelm
added 'use';
1999-02-04, by wenzelm
fail_safe close;
1999-02-04, by wenzelm
check_elem: allow ~, except for '~' and '~~';
1999-02-04, by wenzelm
removed use.ML;
1999-02-04, by wenzelm
removed General/use.ML;
1999-02-04, by wenzelm
made SML/NJ happy;
1999-02-03, by wenzelm
check_thy: include ML stamp;
1999-02-03, by wenzelm
added join_info;
1999-02-03, by wenzelm
tidied load path handling;
1999-02-03, by wenzelm
add_path / reset_path;
1999-02-03, by wenzelm
tuned;
1999-02-03, by wenzelm
ThmDatabase.ml_store_thm;
1999-02-03, by wenzelm
usedir -r;
1999-02-03, by wenzelm
Session.init;
1999-02-03, by wenzelm
Theory loader database: theory and file dependencies, theory values
1999-02-03, by wenzelm
tidied;
1999-02-03, by wenzelm
Session management -- maintain state of logic images.
1999-02-03, by wenzelm
get_lexicon;
1999-02-03, by wenzelm
tokenize: get exploded args;
1999-02-03, by wenzelm
delete_tmpfiles (from thy_read.ML);
1999-02-03, by wenzelm
added reset_path;
1999-02-03, by wenzelm
open BasicThmDatabase;
1999-02-03, by wenzelm
Theory presentation (fake implementation);
1999-02-03, by wenzelm
moved to Pure/context.ML;
1999-02-03, by wenzelm
nuked;
1999-02-03, by wenzelm
moved to General/use.ML;
1999-02-03, by wenzelm
removed load;
1999-02-03, by wenzelm
ThyInfo.begin_theory;
1999-02-03, by wenzelm
oops, update_thy;
1999-02-03, by wenzelm
removed load;
1999-02-03, by wenzelm
removed load;
1999-02-03, by wenzelm
comment;
1999-02-03, by wenzelm
removed load;
1999-02-03, by wenzelm
proper setup of preloaded theories (ThyInfo.register_theory);
1999-02-03, by wenzelm
renamed sig to PRIVATE_SIGN;
1999-02-03, by wenzelm
added thm, thms, Open_locale, Close_locale, Print_scope;
1999-02-03, by wenzelm
added Goal(w) and Export (from context.ML);
1999-02-03, by wenzelm
added is_draft;
1999-02-03, by wenzelm
enabled sig;
1999-02-03, by wenzelm
tuned msg;
1999-02-03, by wenzelm
Global theory context (used to be in Thy/context.ML);
1999-02-03, by wenzelm
moved several files;
1999-02-03, by wenzelm
more abstract implementation;
1999-02-03, by wenzelm
use Path.T;
1999-02-03, by wenzelm
of_file: Path.T, Position.T;
1999-02-03, by wenzelm
added use.ML;
1999-02-03, by wenzelm
added Use;
1999-02-03, by wenzelm
tuned;
1999-02-03, by wenzelm
tidied; added thy_load.ML
1999-02-03, by paulson
tidied, with left_inverse & right_inverse as default simprules
1999-02-03, by paulson
auto update
1999-02-03, by paulson
inj
1999-02-03, by paulson
documented typecheck_tac, etc
1999-02-03, by paulson
standard spelling: type-checking
1999-02-03, by paulson
inj is now a translation of inj_on
1999-02-03, by paulson
standard spelling: type-checking
1999-02-03, by paulson
a bit of tidying
1999-02-01, by paulson
Theory loader primitives.
1999-01-30, by wenzelm
corrected output of symbols for several (probably not all) relevant functions
1999-01-29, by oheimb
renamed space2 to spacespace
1999-01-29, by oheimb
corrected output of symbols for several (probably not all) relevant functions
1999-01-29, by oheimb
moved print_mode to ROOT.ML
1999-01-29, by oheimb
expandshort
1999-01-29, by paulson
expandshort
1999-01-29, by paulson
tidied
1999-01-29, by paulson
tidied
1999-01-28, by paulson
constdefs
1999-01-28, by paulson
tidying
1999-01-28, by paulson
arith_tac for min/max
1999-01-27, by nipkow
*** empty log message ***
1999-01-27, by wenzelm
ZF typechecking
1999-01-27, by paulson
automatic insertion of datatype intr rules into claset
1999-01-27, by paulson
new typechecking solver for the simplifier
1999-01-27, by paulson
tuned;
1999-01-25, by wenzelm
Fixed a bug in lin.arith.
1999-01-24, by nipkow
tuned;
1999-01-22, by wenzelm
tuned;
1999-01-22, by wenzelm
isabelle.in.tum.de;
1999-01-20, by wenzelm
http://isabelle.in.tum.de/dist/;
1999-01-20, by wenzelm
renamed variables for clarity
1999-01-20, by paulson
changed Minho mirror;
1999-01-20, by wenzelm
tidied freeness reasoning
1999-01-19, by paulson
freeness reasoning: T.free_iffs
1999-01-19, by paulson
tuned;
1999-01-19, by wenzelm
removal of the (thm list) argument of mk_cases
1999-01-19, by paulson
tidied; added dest_eq
1999-01-19, by paulson
simplified thanks to the arithmetic prover
1999-01-19, by paulson
updated comments
1999-01-19, by paulson
a simplification by G Bella
1999-01-19, by paulson
structure Graph = Graph;
1999-01-18, by wenzelm
GraphFun (generic directed graphs);
1999-01-18, by wenzelm
added General/graph.ML: generic direct graphs;
1999-01-18, by wenzelm
removed empty line (in case of empty begin_state marker) before Level line
1999-01-15, by oheimb
Removed superfluous arith rules from metric_simps
1999-01-14, by nipkow
More Arith.
1999-01-14, by nipkow
Fixed old bug: selection of constant to be split should depend not just on
1999-01-14, by nipkow
nat_arith_tac -> arith_tac
1999-01-14, by nipkow
More arith refinements.
1999-01-14, by nipkow
less
more
|
(0)
-3000
-1000
-120
+120
+1000
+3000
+10000
+30000
tip