blanchet [Mon, 23 Sep 2013 10:58:37 +0200] rev 53797
note coinduct theorems in "primcorec"
blanchet [Mon, 23 Sep 2013 10:46:40 +0200] rev 53796
tuning
blanchet [Mon, 23 Sep 2013 10:45:26 +0200] rev 53795
generate "simps" from "primcorec"
blanchet [Mon, 23 Sep 2013 10:38:23 +0200] rev 53794
undid copy-paste
blanchet [Mon, 23 Sep 2013 10:34:10 +0200] rev 53793
avoid giving same name to simplifying constructor as to real one (to avoid risks of confusion when reading the code)
blanchet [Mon, 23 Sep 2013 10:31:17 +0200] rev 53792
don't generate empty theorem collections
blanchet [Mon, 23 Sep 2013 10:30:43 +0200] rev 53791
tuned code
blanchet [Mon, 23 Sep 2013 09:48:06 +0200] rev 53790
provide a way to override MaSh's port from configuration file
blanchet [Mon, 23 Sep 2013 09:08:07 +0200] rev 53789
new version of MaSh program, with proper shutdown
wenzelm [Sun, 22 Sep 2013 21:04:53 +0200] rev 53788
tuned proofs;
wenzelm [Sun, 22 Sep 2013 19:50:48 +0200] rev 53787
focus on default component according to jEdit window management;
wenzelm [Sun, 22 Sep 2013 18:42:18 +0200] rev 53786
tuned;
wenzelm [Sun, 22 Sep 2013 18:36:22 +0200] rev 53785
tuned signature;
wenzelm [Sun, 22 Sep 2013 18:07:34 +0200] rev 53784
completion popup for history text field;
imitate view font, for default rendering of symbols;
tuned signature;
wenzelm [Sun, 22 Sep 2013 14:30:34 +0200] rev 53783
clarified location of GUI modules (which depend on Swing of JFX);
wenzelm [Sat, 21 Sep 2013 22:48:52 +0200] rev 53782
repaired latex (cf. 7bb0cf27c243);
wenzelm [Sat, 21 Sep 2013 22:33:42 +0200] rev 53781
tuned proofs;
wenzelm [Sat, 21 Sep 2013 20:58:32 +0200] rev 53780
caret range of active text area counts as visible (e.g. relevant for Output after scrolling outside of text view);
wenzelm [Sat, 21 Sep 2013 20:56:06 +0200] rev 53779
tuned;
wenzelm [Sat, 21 Sep 2013 20:31:03 +0200] rev 53778
proper layered pane at root of parent component, not global view (e.g. relevant for tooltips for detached info windows);
wenzelm [Sat, 21 Sep 2013 19:48:46 +0200] rev 53777
immediate access to some elementary examples;
wenzelm [Sat, 21 Sep 2013 17:37:02 +0200] rev 53776
more front-matter;
wenzelm [Sat, 21 Sep 2013 17:20:08 +0200] rev 53775
clarified logo;
wenzelm [Sat, 21 Sep 2013 17:18:26 +0200] rev 53774
proper text replacement (cf. 747835eb2782);
wenzelm [Sat, 21 Sep 2013 17:08:47 +0200] rev 53773
added canonical screenshot;
wenzelm [Sat, 21 Sep 2013 16:44:31 +0200] rev 53772
removed obsolete README;
open Documentation dockable by default;
wenzelm [Sat, 21 Sep 2013 16:08:17 +0200] rev 53771
tuned;
wenzelm [Sat, 21 Sep 2013 15:23:31 +0200] rev 53770
added/updated material from src/Tools/jEdit/README.html;
wenzelm [Sat, 21 Sep 2013 13:05:54 +0200] rev 53769
basic setup for Isabelle/jEdit documentation;
wenzelm [Sat, 21 Sep 2013 12:03:51 +0200] rev 53768
updated keywords;
blanchet [Fri, 20 Sep 2013 22:39:30 +0200] rev 53767
updated CONTRIBUTORS
blanchet [Fri, 20 Sep 2013 22:39:30 +0200] rev 53766
updated NEWS
blanchet [Fri, 20 Sep 2013 22:39:30 +0200] rev 53765
document option
blanchet [Fri, 20 Sep 2013 22:39:30 +0200] rev 53764
merged "isar_try0" and "isar_minimize" options
blanchet [Fri, 20 Sep 2013 22:39:30 +0200] rev 53763
hardcoded obscure option
blanchet [Fri, 20 Sep 2013 22:39:30 +0200] rev 53762
hard-coded an obscure option
blanchet [Fri, 20 Sep 2013 22:39:30 +0200] rev 53761
use configuration mechanism for low-level tracing
blanchet [Fri, 20 Sep 2013 22:39:30 +0200] rev 53760
moved focus to Isabell/jEdit and away from Proof General
blanchet [Fri, 20 Sep 2013 22:39:30 +0200] rev 53759
took out Waldmeister from list of default provers -- it's usually just visual noise, and its integration in Sledgehammer leaves much to be desired
blanchet [Fri, 20 Sep 2013 22:39:30 +0200] rev 53758
tuning (use a blacklist instead of a whitelist)
blanchet [Fri, 20 Sep 2013 22:39:30 +0200] rev 53757
reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet [Fri, 20 Sep 2013 22:39:30 +0200] rev 53756
MaSh tweaks to facilitate debugging
haftmann [Fri, 20 Sep 2013 20:21:54 +0200] rev 53755
tuned proofs
kuncar [Fri, 20 Sep 2013 17:08:08 +0200] rev 53754
make SML/NJ happy
blanchet [Fri, 20 Sep 2013 16:32:27 +0200] rev 53753
renamed "primcorec" to "primcorecursive", to open the door to a 'theory -> theory' command called "primcorec" (cf. "fun" vs. "function")
blanchet [Fri, 20 Sep 2013 15:42:41 +0200] rev 53752
more primcorec docs
blanchet [Fri, 20 Sep 2013 15:05:47 +0200] rev 53751
added primcorec examples with lambdas
blanchet [Fri, 20 Sep 2013 14:50:06 +0200] rev 53750
more primcorec docs
blanchet [Fri, 20 Sep 2013 14:17:47 +0200] rev 53749
adapted primcorec documentation to reflect the three views
blanchet [Fri, 20 Sep 2013 12:09:06 +0200] rev 53748
updated docs
blanchet [Fri, 20 Sep 2013 12:04:48 +0200] rev 53747
took out spurious attributes (no need for several code equations / simps for thesame constants)
blanchet [Fri, 20 Sep 2013 11:44:30 +0200] rev 53746
have "datatype_new_compat" register induction and recursion theorems in nested case
Andreas Lochbihler [Fri, 20 Sep 2013 10:09:16 +0200] rev 53745
prefer Code.abort over code_abort
blanchet [Fri, 20 Sep 2013 00:08:42 +0200] rev 53744
setting the stage for safe constructor simp rules
blanchet [Thu, 19 Sep 2013 23:54:54 +0200] rev 53743
added TODO
blanchet [Thu, 19 Sep 2013 20:23:08 +0200] rev 53742
made tactic more reliable
blanchet [Thu, 19 Sep 2013 20:03:42 +0200] rev 53741
killed exceptional code that is anyway no longer needed, now that the 'simp' attribute has been taken away -- this solves issues in 'primcorec'
blanchet [Thu, 19 Sep 2013 20:03:41 +0200] rev 53740
cleaner handling of collapse theorems
wenzelm [Thu, 19 Sep 2013 19:35:03 +0200] rev 53739
repaired latex (cf. 84522727f9d3);
blanchet [Thu, 19 Sep 2013 18:59:28 +0200] rev 53738
updated NEWS