Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-240
+240
+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.
removed obsolete nat_induct_tac -- cannot work without;
2008-06-14, by wenzelm
removed obsolete case_split_tac -- cannot work without;
2008-06-14, by wenzelm
removed unused excluded_middle_tac;
2008-06-14, by wenzelm
updated geenrated file;
2008-06-14, by wenzelm
qualified old res_inst_tac variants;
2008-06-14, by wenzelm
proper context for tactics derived from res_inst_tac;
2008-06-14, by wenzelm
updated generated file;
2008-06-14, by wenzelm
obsolete;
2008-06-14, by wenzelm
certify_term: reject qualified frees;
2008-06-14, by wenzelm
removed experimental Poplog/PML support;
2008-06-14, by wenzelm
removed obsolete ML_SUFFIX;
2008-06-14, by wenzelm
removed experimental Poplog/PML support;
2008-06-14, by wenzelm
removed obsolete ML_SUFFIX;
2008-06-14, by wenzelm
removed exotic 'token_translation' command;
2008-06-14, by wenzelm
proper name for LinearQuantifierElim;
2008-06-14, by wenzelm
removed old theorem database;
2008-06-14, by wenzelm
map_const: soft version, no failure here (recovers hiding of consts, because a hidden name is illegal and rejected later);
2008-06-13, by wenzelm
hide: delete all accesses from extra names -- reduces ambiguity in extern;
2008-06-13, by wenzelm
map_const: soft version, no failure here;
2008-06-13, by wenzelm
skolem_fact/thm: uniform numbering, even for singleton list;
2008-06-13, by wenzelm
hide (open);
2008-06-13, by wenzelm
no_notation instead of hide;
2008-06-13, by wenzelm
* Recovered hiding of consts;
2008-06-13, by wenzelm
updated generated file;
2008-06-13, by wenzelm
back to CodeTarget.code_width;
2008-06-13, by wenzelm
hide -> hide (open)
2008-06-13, by nipkow
use regular error function;
2008-06-12, by wenzelm
add lemma finite_image_approx; remove unnecessary sort annotations
2008-06-12, by huffman
change orientation of fix_eqI and convert to rule_format;
2008-06-12, by huffman
export just one setup function;
2008-06-12, by wenzelm
removed obsolete skolem declarations -- done by Theory.at_end;
2008-06-12, by wenzelm
tuned setup;
2008-06-12, by wenzelm
remove unnecessary import of Ffun;
2008-06-12, by huffman
imports Ffun
2008-06-12, by huffman
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
2008-06-12, by wenzelm
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
2008-06-12, by wenzelm
sane versions of (qualified_)thms_of_thy;
2008-06-12, by wenzelm
Facts.dest/export_static: content difference;
2008-06-12, by wenzelm
dest/export_static: content difference;
2008-06-12, by wenzelm
declare_skofuns/skolem: canonical argument order;
2008-06-12, by wenzelm
Facts.dest/export_static: content difference;
2008-06-12, by wenzelm
correction
2008-06-12, by nipkow
tuned
2008-06-12, by nipkow
Removed hide swap
2008-06-12, by nipkow
fixed type
2008-06-12, by nipkow
lemma modified
2008-06-12, by nipkow
typo
2008-06-12, by nipkow
had to add rule: because induct_tac no longer works correctly
2008-06-12, by nipkow
Hid swap
2008-06-12, by nipkow
some reformatting;
2008-06-12, by wenzelm
added CK_Machine to the nominal section
2008-06-12, by urbanc
soundness and completeness proofs for a CK machine as
2008-06-12, by urbanc
emoved the parts that deal with the CK machine to a new theory
2008-06-12, by urbanc
tuned header and comments
2008-06-12, by urbanc
OldGoals.inst;
2008-06-11, by wenzelm
Drule.read_instantiate;
2008-06-11, by wenzelm
qualified inst;
2008-06-11, by wenzelm
qualified types_sorts, read_insts etc.;
2008-06-11, by wenzelm
Drule.types_sorts;
2008-06-11, by wenzelm
OldGoals.inst;
2008-06-11, by wenzelm
Drule.read_instantiate;
2008-06-11, by wenzelm
changed pred_congs: merely cover pred1_cong pred2_cong pred3_cong;
2008-06-11, by wenzelm
removed obsolete/unused pred_congs;
2008-06-11, by wenzelm
tuned comments;
2008-06-11, by wenzelm
converted ML proofs from simpdata.ML;
2008-06-11, by wenzelm
removed dead code;
2008-06-11, by wenzelm
RuleInsts.res_inst_tac with proper context;
2008-06-11, by wenzelm
more antiquotations;
2008-06-11, by wenzelm
tuned;
2008-06-11, by wenzelm
explicit rule for induct_tac
2008-06-11, by haftmann
tuned spacing;
2008-06-10, by wenzelm
updated generated file;
2008-06-10, by wenzelm
* Attributes cases, induct, coinduct support del option.
2008-06-10, by wenzelm
added del attributes;
2008-06-10, by wenzelm
back to original import order -- thanks to proper deletion of nat cases/induct rules from type_definition;
2008-06-10, by wenzelm
proper deletion of nat cases/induct rules from type_definition;
2008-06-10, by wenzelm
fixed spelling (Where is WordExamples.thy anyway?);
2008-06-10, by wenzelm
recovered nat_induct as default for induct_tac;
2008-06-10, by wenzelm
more robust declaration of nat_induct;
2008-06-10, by wenzelm
reordering of imports ensures that nat_induct stay in front;
2008-06-10, by wenzelm
adhoc fix of induct_tac: rule nat_induct;
2008-06-10, by wenzelm
case_tac: accomodate change in bound variable name;
2008-06-10, by wenzelm
nat_induct_tac (works without context);
2008-06-10, by wenzelm
moved case_tac/induct_tac to induct_tacs.ML -- no longer hardwired into datatype package;
2008-06-10, by wenzelm
added nat_induct_tac (works without context);
2008-06-10, by wenzelm
InductTacs.case_tac with proper context and proper declaration of local variable;
2008-06-10, by wenzelm
added HOL/Tools/induct_tacs.ML;
2008-06-10, by wenzelm
eliminated obsolete case_split_thm -- use case_split;
2008-06-10, by wenzelm
tuned proofs -- case_tac *is* available here;
2008-06-10, by wenzelm
updated generated file;
2008-06-10, by wenzelm
case_tac/induct_tac: use same declarations as cases/induct;
2008-06-10, by wenzelm
proper news header;
2008-06-10, by wenzelm
removed obsolete read_idents;
2008-06-10, by wenzelm
added (e)res_inst_tac;
2008-06-10, by wenzelm
focus: actually declare constraints for local parameters;
2008-06-10, by wenzelm
tuned proofs;
2008-06-10, by wenzelm
case_split_tac (works without context);
2008-06-10, by wenzelm
tuned;
2008-06-10, by wenzelm
eliminated obsolete case_split_thm -- use case_split;
2008-06-10, by wenzelm
Unstructured induction and cases analysis for Isabelle/HOL.
2008-06-10, by wenzelm
dropped instance with attached definitions
2008-06-10, by haftmann
polished interface of datatype package
2008-06-10, by haftmann
adjusted some proofs involving inats
2008-06-10, by haftmann
refactoring; addition, numerals
2008-06-10, by haftmann
more instantiation
2008-06-10, by haftmann
whitespace tuning
2008-06-10, by haftmann
localized Least in Orderings.thy
2008-06-10, by haftmann
removed some dubious code lemmas
2008-06-10, by haftmann
slightly tuning of some proofs involving case distinction and induction on natural numbers and similar
2008-06-10, by haftmann
rep_datatype command now takes list of constructors as input arguments
2008-06-10, by haftmann
major refactorings in code generator modules
2008-06-10, by haftmann
updated
2008-06-10, by haftmann
slightly tuning of some proofs involving case distinction and induction on natural numbers and similar
2008-06-10, by haftmann
DatatypePackage.case_tac;
2008-06-09, by wenzelm
DatatypePackage.distinct_simproc;
2008-06-09, by wenzelm
DatatypePackage.case_tac;
2008-06-09, by wenzelm
signature cleanup -- no pervasives anymore;
2008-06-09, by wenzelm
qualified DatatypePackage.distinct_simproc;
2008-06-09, by wenzelm
adapted case_tac/induct_tac;
2008-06-09, by wenzelm
updated generated file;
Isabelle2008
2008-06-08, by wenzelm
minor typos;
2008-06-08, by wenzelm
simp: depth_limit is now a configuration option;
2008-06-08, by wenzelm
removed old AxClass;
2008-06-08, by wenzelm
remove codegen_process.pdf from distribution;
2008-06-08, by wenzelm
fixed wrong treatment of type variables in instantiation target
2008-06-07, by haftmann
switched to Poly/ML 5.2;
2008-06-06, by wenzelm
doc test now runs on linux
2008-06-06, by isatest
added at-poly-5.1-para-e;
2008-06-05, by wenzelm
adjusted location of cambridge website
2008-06-05, by haftmann
switch from gtar to tar
2008-06-05, by isatest
send from linux systems as well
2008-06-05, by isatest
tikz: change to pgfsys-dvi.def for plain dvi output;
2008-06-04, by wenzelm
replaced (*<*)(*>*) by invisibility tags;
2008-06-04, by wenzelm
updated generated file;
2008-06-04, by wenzelm
updated generated file;
2008-06-04, by wenzelm
work within *this* directory;
2008-06-04, by wenzelm
moved labels into actual sections;
2008-06-04, by wenzelm
removed TEXPATH, just chdir to Locales/document;
2008-06-04, by wenzelm
renamed expression: plain ~ (space) instead of \colon;
2008-06-04, by wenzelm
updated generated file;
2008-06-04, by wenzelm
replaced strange \: by \colon to make it work again on macbroy20-29;
2008-06-04, by wenzelm
updated generated file;
2008-06-03, by wenzelm
clarification of "subst" by Lucas Dixon;
2008-06-03, by wenzelm
use polyml-5.2;
2008-06-03, by wenzelm
updated to official 5.2;
2008-06-03, by wenzelm
use isabelle style files from Doc/ -- not the generated ones (which are not present in the repository anyway);
2008-06-03, by wenzelm
some reorganization and fine-tuning;
2008-06-03, by wenzelm
some fine-tuning;
2008-06-03, by wenzelm
CodeTarget.target_code_width;
2008-06-03, by wenzelm
Tuned proof.
2008-06-03, by ballarin
New version covering interpretation.
2008-06-03, by ballarin
proper path to isabelle.jar;
2008-06-03, by wenzelm
reorganized isar-ref;
2008-06-03, by wenzelm
added Wenzel:2006:Festschrift;
2008-06-03, by wenzelm
class_deps: improper;
2008-06-03, by wenzelm
\cite{Wenzel:2006:Festschrift};
2008-06-03, by wenzelm
updated generated file;
2008-06-03, by wenzelm
moved stuff from pure.thy to Misc.thy;
2008-06-03, by wenzelm
obsolete;
2008-06-03, by wenzelm
updated generated file;
2008-06-03, by wenzelm
tuned;
2008-06-03, by wenzelm
updated generated file;
2008-06-02, by wenzelm
moved header command to Document_Preparation;
2008-06-02, by wenzelm
tuned structure;
2008-06-02, by wenzelm
moved header command here;
2008-06-02, by wenzelm
removed onsolete pure.thy (cf. Misc.thy);
2008-06-02, by wenzelm
updated generated file;
2008-06-02, by wenzelm
updated ML types for advanced translations;
2008-06-02, by wenzelm
moved (ax_)specification to end;
2008-06-02, by wenzelm
moved subst/hypsubst to "Basic proof tools";
2008-06-02, by wenzelm
added Document_Preparation;
2008-06-02, by wenzelm
updated generated file;
2008-06-02, by wenzelm
tuned spacing;
2008-06-02, by wenzelm
major reorganization of document structure;
2008-06-02, by wenzelm
removed obsolete basics.tex;
2008-06-02, by wenzelm
more contributors;
2008-06-02, by wenzelm
renamed theory "syntax" to "Outer_Syntax";
2008-06-02, by wenzelm
isatool tty;
2008-06-02, by wenzelm
renamed theory "intro" to "Introduction";
2008-06-02, by wenzelm
tuned proofs
2008-06-02, by nipkow
fixed bug: maxidx was wrongly calculuated from term, now calculated
2008-06-01, by dixon
new example
2008-06-01, by urbanc
updated to E 0.999-006;
2008-05-31, by wenzelm
THIS_IS_ISABELLE_MAKEBIN is back;
2008-05-30, by wenzelm
cvs2cl only for unofficial releases;
2008-05-30, by wenzelm
more AFP sessions;
2008-05-30, by wenzelm
*** empty log message ***
2008-05-30, by nipkow
Updated function tutorial.
2008-05-30, by krauss
(adjusted)
2008-05-30, by haftmann
various code streamlining
2008-05-30, by haftmann
more AFP sessions;
2008-05-30, by wenzelm
legacy_feature: no proof context in simpset;
2008-05-29, by wenzelm
proper context for attribute simplified;
2008-05-29, by wenzelm
added warning_count for issued reconstruction failure messages (limit 10);
2008-05-29, by wenzelm
proper context for ss;
2008-05-29, by wenzelm
proper context for simp_thms_conv;
2008-05-29, by wenzelm
added warning_count for issued reconstruction failure messages;
2008-05-29, by wenzelm
tuned;
2008-05-29, by wenzelm
*** empty log message ***
2008-05-29, by nipkow
yet another attempt to circumvent printmode problems
2008-05-29, by haftmann
obsolete;
2008-05-28, by wenzelm
moved README-polyml to polyml/README;
2008-05-28, by wenzelm
README for Poly/ML 5.2 distribution;
2008-05-28, by wenzelm
tuned;
2008-05-28, by wenzelm
more contribs;
2008-05-28, by wenzelm
misc tuning for Isabelle2008;
2008-05-28, by wenzelm
added some notable improvements;
2008-05-28, by wenzelm
tuned version numbers;
2008-05-28, by wenzelm
prepared for Isabelle2008;
2008-05-28, by wenzelm
added ISABELLE_HOME to startup;
2008-05-28, by wenzelm
added Substring.full;
2008-05-28, by wenzelm
moved distinctness_limit to datatype_rep_proofs.ML
2008-05-28, by haftmann
fixed utterly wrong print mode handling
2008-05-28, by haftmann
new serializer interface
2008-05-28, by haftmann
added new code_datatype example
2008-05-28, by haftmann
proper use of the Pretty module
2008-05-26, by haftmann
permissive wrt. instantiation of class operations
2008-05-26, by haftmann
proper lemma [source] antiquotation
2008-05-26, by haftmann
check for illegal merge of class parameters
2008-05-26, by haftmann
proper NoSubsort CLASS_ERROR
2008-05-26, by haftmann
tuned theorem order
2008-05-26, by haftmann
inst_subst_tac: match types -- no longer assume that subst rule has exactly one type argument;
2008-05-24, by wenzelm
updated generated file;
2008-05-24, by wenzelm
added local_theory command wrappers;
2008-05-24, by wenzelm
uniform treatment of target, not as config;
2008-05-24, by wenzelm
more uniform treatment of OuterSyntax.local_theory commands;
2008-05-24, by wenzelm
updated generated file;
2008-05-24, by wenzelm
invisible comment;
2008-05-24, by wenzelm
function: uniform treatment of target, not as config;
2008-05-24, by wenzelm
added parse_document (optional unchecked header material);
2008-05-24, by wenzelm
exported master_directory;
2008-05-24, by wenzelm
present_excursion: setmp_thread_position during presentation;
2008-05-24, by wenzelm
use: explicit .ML;
2008-05-24, by wenzelm
ident: naive caching prevents potentially slow external invocations;
2008-05-24, by wenzelm
fixed improper handling of return code (pdf and ps.gz formats)
2008-05-24, by urbanc
add constants: set Markup.theory_nameN in tags;
2008-05-23, by wenzelm
added theory_nameN;
2008-05-23, by wenzelm
rearranged subsections
2008-05-23, by krauss
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
2008-05-23, by berghofe
Replaced Pretty.str and Pretty.string_of by specific functions that
2008-05-23, by berghofe
less
more
|
(0)
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
+30000
tip