Mercurial Mercurial > repos > isabelle / changelog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -30000 -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.
Wed, 24 Apr 2013 12:15:06 +0200 took out workaround for bug fixed in 5af40820948b
changeset
traytel [Wed, 24 Apr 2013 12:15:06 +0200] rev 51753
took out workaround for bug fixed in 5af40820948b
Wed, 24 Apr 2013 11:36:11 +0200 merged
changeset
traytel [Wed, 24 Apr 2013 11:36:11 +0200] rev 51752
merged
Wed, 24 Apr 2013 11:06:53 +0200 slightly more aggressive syntax translation for printing case expressions
changeset
traytel [Wed, 24 Apr 2013 11:06:53 +0200] rev 51751
slightly more aggressive syntax translation for printing case expressions
Wed, 24 Apr 2013 11:32:54 +0200 avoid odd reinit after sublocale declaration
changeset
haftmann [Wed, 24 Apr 2013 11:32:54 +0200] rev 51750
avoid odd reinit after sublocale declaration
Wed, 24 Apr 2013 10:23:47 +0200 moved defs into locale to reduce unnecessary polymorphism; tuned
changeset
nipkow [Wed, 24 Apr 2013 10:23:47 +0200] rev 51749
moved defs into locale to reduce unnecessary polymorphism; tuned
Tue, 23 Apr 2013 19:40:33 +0200 dropped dead code
changeset
haftmann [Tue, 23 Apr 2013 19:40:33 +0200] rev 51748
dropped dead code
Tue, 23 Apr 2013 19:31:24 +0200 documentation and NEWS
changeset
haftmann [Tue, 23 Apr 2013 19:31:24 +0200] rev 51747
documentation and NEWS
Tue, 23 Apr 2013 17:46:12 +0200 avoid accidental specialization of the types in the "map" property of codatatypes
changeset
blanchet [Tue, 23 Apr 2013 17:46:12 +0200] rev 51746
avoid accidental specialization of the types in the "map" property of codatatypes
Tue, 23 Apr 2013 17:15:44 +0200 simplify "Inl () = Inr ()" as well (not entirely clear why this is necessary)
changeset
blanchet [Tue, 23 Apr 2013 17:15:44 +0200] rev 51745
simplify "Inl () = Inr ()" as well (not entirely clear why this is necessary)
Tue, 23 Apr 2013 17:13:14 +0200 more examples
changeset
blanchet [Tue, 23 Apr 2013 17:13:14 +0200] rev 51744
more examples
Tue, 23 Apr 2013 16:49:14 +0200 tuning
changeset
blanchet [Tue, 23 Apr 2013 16:49:14 +0200] rev 51743
tuning
Tue, 23 Apr 2013 16:41:59 +0200 fix bugs in expand tactic w.r.t. datatypes with "needless" discriminators (e.g. lists with is_Nil instead of ~= Nil)
changeset
blanchet [Tue, 23 Apr 2013 16:41:59 +0200] rev 51742
fix bugs in expand tactic w.r.t. datatypes with "needless" discriminators (e.g. lists with is_Nil instead of ~= Nil)
Tue, 23 Apr 2013 16:30:30 +0200 tuning
changeset
blanchet [Tue, 23 Apr 2013 16:30:30 +0200] rev 51741
tuning
Tue, 23 Apr 2013 16:30:29 +0200 tuned_comment
changeset
blanchet [Tue, 23 Apr 2013 16:30:29 +0200] rev 51740
tuned_comment
Tue, 23 Apr 2013 11:43:09 +0200 (co)rec is (just as the (un)fold) the unique morphism;
changeset
traytel [Tue, 23 Apr 2013 11:43:09 +0200] rev 51739
(co)rec is (just as the (un)fold) the unique morphism;
Tue, 23 Apr 2013 11:14:51 +0200 tuned: unnamed contexts, interpretation and sublocale in locale target;
changeset
haftmann [Tue, 23 Apr 2013 11:14:51 +0200] rev 51738
tuned: unnamed contexts, interpretation and sublocale in locale target; corrected slip in List.thy: setsum requires commmutativity
Tue, 23 Apr 2013 11:14:50 +0200 target-sensitive user-level commands interpretation and sublocale
changeset
haftmann [Tue, 23 Apr 2013 11:14:50 +0200] rev 51737
target-sensitive user-level commands interpretation and sublocale
Tue, 23 Apr 2013 11:14:50 +0200 ML interfaces for various kinds of interpretation
changeset
haftmann [Tue, 23 Apr 2013 11:14:50 +0200] rev 51736
ML interfaces for various kinds of interpretation
Tue, 23 Apr 2013 11:14:50 +0200 brittleness stamping for local theories
changeset
haftmann [Tue, 23 Apr 2013 11:14:50 +0200] rev 51735
brittleness stamping for local theories
Tue, 23 Apr 2013 11:14:50 +0200 tuned
changeset
haftmann [Tue, 23 Apr 2013 11:14:50 +0200] rev 51734
tuned
Mon, 22 Apr 2013 18:39:12 +0200 removed type constraints
changeset
immler [Mon, 22 Apr 2013 18:39:12 +0200] rev 51733
removed type constraints
Mon, 22 Apr 2013 16:36:02 +0200 NEWS
changeset
hoelzl [Mon, 22 Apr 2013 16:36:02 +0200] rev 51732
NEWS
Sun, 21 Apr 2013 20:08:13 +0200 more sharing
changeset
haftmann [Sun, 21 Apr 2013 20:08:13 +0200] rev 51731
more sharing
Sun, 21 Apr 2013 16:29:40 +0200 interpretation: distinguish theories and proofs by explicit parameter rather than generic context;
changeset
haftmann [Sun, 21 Apr 2013 16:29:40 +0200] rev 51730
interpretation: distinguish theories and proofs by explicit parameter rather than generic context; formal initialisation of theory target during interpretation; prefer Local_Theory.notes_kind to register mixin equations during interpretation; more uniformity between note_eqns_register and note_eqns_dependency
Sun, 21 Apr 2013 10:41:18 +0200 dropped unusued identifier
changeset
haftmann [Sun, 21 Apr 2013 10:41:18 +0200] rev 51729
dropped unusued identifier
Sun, 21 Apr 2013 10:41:18 +0200 avoid odd bifurcation with Attrib.local_notes vs. Locale.add_thmss -- n.b. note_eqns_dependency operates in a specific locale target
changeset
haftmann [Sun, 21 Apr 2013 10:41:18 +0200] rev 51728
avoid odd bifurcation with Attrib.local_notes vs. Locale.add_thmss -- n.b. note_eqns_dependency operates in a specific locale target
Sun, 21 Apr 2013 10:41:18 +0200 tuned for uniformity
changeset
haftmann [Sun, 21 Apr 2013 10:41:18 +0200] rev 51727
tuned for uniformity
Sun, 21 Apr 2013 10:41:18 +0200 reflection as official HOL tool
changeset
haftmann [Sun, 21 Apr 2013 10:41:18 +0200] rev 51726
reflection as official HOL tool
Sun, 21 Apr 2013 10:41:18 +0200 follow Isabelle spacing praxis more thoroughly
changeset
haftmann [Sun, 21 Apr 2013 10:41:18 +0200] rev 51725
follow Isabelle spacing praxis more thoroughly
Sun, 21 Apr 2013 10:41:18 +0200 honour FIXMEs as far as feasible at the moment
changeset
haftmann [Sun, 21 Apr 2013 10:41:18 +0200] rev 51724
honour FIXMEs as far as feasible at the moment
Sun, 21 Apr 2013 10:41:18 +0200 combined reify_data.ML into reflection.ML;
changeset
haftmann [Sun, 21 Apr 2013 10:41:18 +0200] rev 51723
combined reify_data.ML into reflection.ML; attempt to establish a more accessible and more consistent terminology; more ML code in ML file rather than setup theory; ML slightly tuned wrt. Isabelle coding conventions
Sat, 20 Apr 2013 20:57:49 +0200 proved termination for fun-based AI
changeset
nipkow [Sat, 20 Apr 2013 20:57:49 +0200] rev 51722
proved termination for fun-based AI
Sat, 20 Apr 2013 19:30:04 +0200 tuned
changeset
nipkow [Sat, 20 Apr 2013 19:30:04 +0200] rev 51721
tuned
Fri, 19 Apr 2013 12:04:57 +0200 tuned
changeset
nipkow [Fri, 19 Apr 2013 12:04:57 +0200] rev 51720
tuned
Thu, 18 Apr 2013 21:31:24 +0200 merged
changeset
wenzelm [Thu, 18 Apr 2013 21:31:24 +0200] rev 51719
merged
Thu, 18 Apr 2013 21:10:12 +0200 tuned signature;
changeset
wenzelm [Thu, 18 Apr 2013 21:10:12 +0200] rev 51718
tuned signature;
Thu, 18 Apr 2013 17:07:01 +0200 simplifier uses proper Proof.context instead of historic type simpset;
changeset
wenzelm [Thu, 18 Apr 2013 17:07:01 +0200] rev 51717
simplifier uses proper Proof.context instead of historic type simpset;
Thu, 18 Apr 2013 20:18:50 +0200 merged
changeset
nipkow [Thu, 18 Apr 2013 20:18:50 +0200] rev 51716
merged
Thu, 18 Apr 2013 20:18:37 +0200 avoided map_of in def of fun_rep (but still needed for efficient code)
changeset
nipkow [Thu, 18 Apr 2013 20:18:37 +0200] rev 51715
avoided map_of in def of fun_rep (but still needed for efficient code)
Thu, 18 Apr 2013 18:57:02 +0200 spelling
changeset
haftmann [Thu, 18 Apr 2013 18:57:02 +0200] rev 51714
spelling
Thu, 18 Apr 2013 18:55:23 +0200 spelling
changeset
haftmann [Thu, 18 Apr 2013 18:55:23 +0200] rev 51713
spelling
Wed, 17 Apr 2013 21:23:35 +0200 tuned
changeset
nipkow [Wed, 17 Apr 2013 21:23:35 +0200] rev 51712
tuned
Wed, 17 Apr 2013 21:11:01 +0200 complete revision: finally got rid of annoying L-predicate
changeset
nipkow [Wed, 17 Apr 2013 21:11:01 +0200] rev 51711
complete revision: finally got rid of annoying L-predicate
Wed, 17 Apr 2013 20:53:26 +0200 moved leastness lemma
changeset
nipkow [Wed, 17 Apr 2013 20:53:26 +0200] rev 51710
moved leastness lemma
Tue, 16 Apr 2013 17:54:14 +0200 proper prolog command-line instead of hashbang, which might switch to invalid executable and thus fail (notably on lxbroy2);
changeset
wenzelm [Tue, 16 Apr 2013 17:54:14 +0200] rev 51709
proper prolog command-line instead of hashbang, which might switch to invalid executable and thus fail (notably on lxbroy2); speculative update for yap (untested);
Mon, 15 Apr 2013 22:51:55 +0200 use automatic type coerctions in Sqrt example
changeset
hoelzl [Mon, 15 Apr 2013 22:51:55 +0200] rev 51708
use automatic type coerctions in Sqrt example
Mon, 15 Apr 2013 12:03:16 +0200 make SML/NJ happy;
changeset
wenzelm [Mon, 15 Apr 2013 12:03:16 +0200] rev 51707
make SML/NJ happy;
Mon, 15 Apr 2013 10:41:03 +0200 not all Nitpick 'constructors' are injective -- careful
changeset
blanchet [Mon, 15 Apr 2013 10:41:03 +0200] rev 51706
not all Nitpick 'constructors' are injective -- careful
Sun, 14 Apr 2013 21:54:45 +1000 added another definition snipped
changeset
kleing [Sun, 14 Apr 2013 21:54:45 +1000] rev 51705
added another definition snipped
Fri, 12 Apr 2013 17:56:51 +0200 actually fail on prolog errors -- such as swipl startup failure due to missing shared libraries -- assuming it normally produces clean return code 0;
changeset
wenzelm [Fri, 12 Apr 2013 17:56:51 +0200] rev 51704
actually fail on prolog errors -- such as swipl startup failure due to missing shared libraries -- assuming it normally produces clean return code 0;
Fri, 12 Apr 2013 17:21:51 +0200 modifiers for classical wrappers operate on Proof.context instead of claset;
changeset
wenzelm [Fri, 12 Apr 2013 17:21:51 +0200] rev 51703
modifiers for classical wrappers operate on Proof.context instead of claset;
Fri, 12 Apr 2013 17:02:55 +0200 removed historic comments;
changeset
wenzelm [Fri, 12 Apr 2013 17:02:55 +0200] rev 51702
removed historic comments;
Fri, 12 Apr 2013 15:30:38 +0200 tuned exceptions -- avoid composing error messages in low-level situations;
changeset
wenzelm [Fri, 12 Apr 2013 15:30:38 +0200] rev 51701
tuned exceptions -- avoid composing error messages in low-level situations;
Fri, 12 Apr 2013 14:54:14 +0200 tuned signature;
changeset
wenzelm [Fri, 12 Apr 2013 14:54:14 +0200] rev 51700
tuned signature; tuned comments;
Fri, 12 Apr 2013 12:20:51 +0200 proper identifiers -- avoid crash of case translations;
changeset
wenzelm [Fri, 12 Apr 2013 12:20:51 +0200] rev 51699
proper identifiers -- avoid crash of case translations;
Fri, 12 Apr 2013 08:27:43 +0200 reduced duplication
changeset
nipkow [Fri, 12 Apr 2013 08:27:43 +0200] rev 51698
reduced duplication
Thu, 11 Apr 2013 16:58:54 +0200 do not add case translation syntax in rep_datatype compatibility mode
changeset
traytel [Thu, 11 Apr 2013 16:58:54 +0200] rev 51697
do not add case translation syntax in rep_datatype compatibility mode
Thu, 11 Apr 2013 16:39:01 +0200 run type inference on input to wrap_data
changeset
traytel [Thu, 11 Apr 2013 16:39:01 +0200] rev 51696
run type inference on input to wrap_data
Thu, 11 Apr 2013 16:03:11 +0200 installed case translations in BNF package
changeset
traytel [Thu, 11 Apr 2013 16:03:11 +0200] rev 51695
installed case translations in BNF package
Thu, 11 Apr 2013 15:10:22 +0200 tuned
changeset
nipkow [Thu, 11 Apr 2013 15:10:22 +0200] rev 51694
tuned
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip
isabelle