Mercurial
Mercurial
>
repos
>
isabelle
/ file revisions
summary
|
shortlog
|
changelog
|
graph
|
tags
|
bookmarks
|
branches
|
file
| revisions |
annotate
|
diff
|
comparison
|
rss
|
help
(0)
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
src/Sequents/simpdata.ML
2012-01-11
wenzelm
more qualified names;
file
|
diff
|
annotate
2011-11-28
wenzelm
avoid stepping outside of context -- plain zero_var_indexes should be sufficient;
file
|
diff
|
annotate
2011-11-24
wenzelm
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
file
|
diff
|
annotate
2011-11-23
wenzelm
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
file
|
diff
|
annotate
2011-06-29
wenzelm
tuned signature;
file
|
diff
|
annotate
2011-06-29
wenzelm
simplified/unified Simplifier.mk_solver;
file
|
diff
|
annotate
2011-05-13
wenzelm
clarified map_simpset versus Simplifier.map_simpset_global;
file
|
diff
|
annotate
2010-08-17
haftmann
more antiquotations
file
|
diff
|
annotate
2010-04-30
wenzelm
proper context for rule_by_tactic;
file
|
diff
|
annotate
2010-04-29
wenzelm
proper context for mksimps etc. -- via simpset of the running Simplifier;
file
|
diff
|
annotate
2010-03-13
wenzelm
removed old CVS Ids;
file
|
diff
|
annotate
2010-02-19
wenzelm
renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
file
|
diff
|
annotate
2010-02-07
wenzelm
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
file
|
diff
|
annotate
2009-10-16
wenzelm
explicitly qualify Drule.standard;
file
|
diff
|
annotate
2009-07-23
wenzelm
more @{theory} antiquotations;
file
|
diff
|
annotate
2009-07-20
wenzelm
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
file
|
diff
|
annotate
2008-06-11
wenzelm
converted ML proofs from simpdata.ML;
file
|
diff
|
annotate
2008-05-17
wenzelm
structure Display: less pervasive operations;
file
|
diff
|
annotate
2007-05-09
wenzelm
tuned ML setup;
file
|
diff
|
annotate
2006-11-20
wenzelm
removed legacy ML setup;
file
|
diff
|
annotate
2006-11-20
wenzelm
converted legacy ML scripts;
file
|
diff
|
annotate
2005-10-18
wenzelm
Simplifier.theory_context;
file
|
diff
|
annotate
2005-10-17
wenzelm
change_claset/simpset;
file
|
diff
|
annotate
2005-09-18
wenzelm
converted to Isar theory format;
file
|
diff
|
annotate
2002-01-12
wenzelm
renamed forall_elim_vars_safe to gen_all;
file
|
diff
|
annotate
2002-01-11
wenzelm
replace gen_all by forall_elim_vars_safe;
file
|
diff
|
annotate
2000-08-28
wenzelm
cong setup now part of Simplifier;
file
|
diff
|
annotate
2000-07-06
paulson
removal of batch style, and tidying
file
|
diff
|
annotate
1999-09-21
nipkow
Mod because of new solver interface.
file
|
diff
|
annotate
1999-07-28
paulson
congruence rule for |-, etc.
file
|
diff
|
annotate
less
more
(0)
tip