Wed, 10 Oct 2012 12:12:27 +0200 add induction rule for intersection-stable sigma-sets
hoelzl [Wed, 10 Oct 2012 12:12:27 +0200] rev 49789
add induction rule for intersection-stable sigma-sets
Wed, 10 Oct 2012 12:12:26 +0200 show and use distributed_swap and distributed_jointI
hoelzl [Wed, 10 Oct 2012 12:12:26 +0200] rev 49788
show and use distributed_swap and distributed_jointI
Wed, 10 Oct 2012 12:12:25 +0200 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl [Wed, 10 Oct 2012 12:12:25 +0200] rev 49787
rule to show that conditional mutual information is non-negative in the continuous case
Wed, 10 Oct 2012 12:12:25 +0200 continuous version of entropy_le
hoelzl [Wed, 10 Oct 2012 12:12:25 +0200] rev 49786
continuous version of entropy_le
Wed, 10 Oct 2012 12:12:24 +0200 simplified entropy_uniform
hoelzl [Wed, 10 Oct 2012 12:12:24 +0200] rev 49785
simplified entropy_uniform
Wed, 10 Oct 2012 12:12:23 +0200 remove incseq assumption from measure_eqI_generator_eq
hoelzl [Wed, 10 Oct 2012 12:12:23 +0200] rev 49784
remove incseq assumption from measure_eqI_generator_eq
Wed, 10 Oct 2012 12:12:23 +0200 generalize from prob_space to finite_measure
hoelzl [Wed, 10 Oct 2012 12:12:23 +0200] rev 49783
generalize from prob_space to finite_measure
Wed, 10 Oct 2012 12:12:22 +0200 add measurable_compose
hoelzl [Wed, 10 Oct 2012 12:12:22 +0200] rev 49782
add measurable_compose
Wed, 10 Oct 2012 12:12:21 +0200 simplified assumptions for kolmogorov_0_1_law
hoelzl [Wed, 10 Oct 2012 12:12:21 +0200] rev 49781
simplified assumptions for kolmogorov_0_1_law
Wed, 10 Oct 2012 12:12:21 +0200 merge should operate on pairs
hoelzl [Wed, 10 Oct 2012 12:12:21 +0200] rev 49780
merge should operate on pairs
Wed, 10 Oct 2012 12:12:20 +0200 remove incseq assumption from sigma_prod_algebra_sigma_eq
hoelzl [Wed, 10 Oct 2012 12:12:20 +0200] rev 49779
remove incseq assumption from sigma_prod_algebra_sigma_eq
Wed, 10 Oct 2012 12:12:19 +0200 sigma_finite_iff_density_finite does not require a positive density function
hoelzl [Wed, 10 Oct 2012 12:12:19 +0200] rev 49778
sigma_finite_iff_density_finite does not require a positive density function
Wed, 10 Oct 2012 12:12:18 +0200 tuned Lebesgue measure proofs
hoelzl [Wed, 10 Oct 2012 12:12:18 +0200] rev 49777
tuned Lebesgue measure proofs
Wed, 10 Oct 2012 12:12:18 +0200 tuned product measurability
hoelzl [Wed, 10 Oct 2012 12:12:18 +0200] rev 49776
tuned product measurability
Wed, 10 Oct 2012 12:12:17 +0200 remove some unneeded positivity assumptions; generalize some assumptions to AE; tuned proofs
hoelzl [Wed, 10 Oct 2012 12:12:17 +0200] rev 49775
remove some unneeded positivity assumptions; generalize some assumptions to AE; tuned proofs
Wed, 10 Oct 2012 12:12:16 +0200 use continuity to show Borel-measurability
hoelzl [Wed, 10 Oct 2012 12:12:16 +0200] rev 49774
use continuity to show Borel-measurability
Wed, 10 Oct 2012 12:12:15 +0200 tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl [Wed, 10 Oct 2012 12:12:15 +0200] rev 49773
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
Wed, 10 Oct 2012 12:12:14 +0200 rename terminal_events to tail_event
hoelzl [Wed, 10 Oct 2012 12:12:14 +0200] rev 49772
rename terminal_events to tail_event
Wed, 10 Oct 2012 13:04:15 +0200 merged
Andreas Lochbihler [Wed, 10 Oct 2012 13:04:15 +0200] rev 49771
merged
Wed, 10 Oct 2012 13:03:50 +0200 efficient construction of red black trees from sorted associative lists
Andreas Lochbihler [Wed, 10 Oct 2012 13:03:50 +0200] rev 49770
efficient construction of red black trees from sorted associative lists
Wed, 10 Oct 2012 12:52:24 +0200 more explicit code equations
haftmann [Wed, 10 Oct 2012 12:52:24 +0200] rev 49769
more explicit code equations
Wed, 10 Oct 2012 10:48:55 +0200 adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc
bulwahn [Wed, 10 Oct 2012 10:48:55 +0200] rev 49768
adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc
Wed, 10 Oct 2012 10:48:33 +0200 special code setup for step function in IMP is redundant as definition was tuned (cf. c54d901d2946)
bulwahn [Wed, 10 Oct 2012 10:48:33 +0200] rev 49767
special code setup for step function in IMP is redundant as definition was tuned (cf. c54d901d2946)
Wed, 10 Oct 2012 10:48:17 +0200 test case for set_comprehension_pointfree simproc succeeds now
bulwahn [Wed, 10 Oct 2012 10:48:17 +0200] rev 49766
test case for set_comprehension_pointfree simproc succeeds now
Wed, 10 Oct 2012 10:47:52 +0200 unfolding bounded existential quantifiers as first step in the set_comprehension_pointfree simproc
bulwahn [Wed, 10 Oct 2012 10:47:52 +0200] rev 49765
unfolding bounded existential quantifiers as first step in the set_comprehension_pointfree simproc
Wed, 10 Oct 2012 10:47:43 +0200 moving simproc from Finite_Set to more appropriate Product_Type theory
bulwahn [Wed, 10 Oct 2012 10:47:43 +0200] rev 49764
moving simproc from Finite_Set to more appropriate Product_Type theory
Wed, 10 Oct 2012 10:47:21 +0200 generalizing set_comprehension_pointfree simproc to work for arbitrary predicates (and not just the finite predicate)
bulwahn [Wed, 10 Oct 2012 10:47:21 +0200] rev 49763
generalizing set_comprehension_pointfree simproc to work for arbitrary predicates (and not just the finite predicate)
Wed, 10 Oct 2012 10:41:18 +0200 adding some example that motivates some of the current changes in the set_comprehension_pointfree simproc
bulwahn [Wed, 10 Oct 2012 10:41:18 +0200] rev 49762
adding some example that motivates some of the current changes in the set_comprehension_pointfree simproc
Wed, 10 Oct 2012 10:41:16 +0200 set_comprehension_pointfree also handles terms where the equation is not at the first position, which is a necessary generalisation to eventually handle bounded existentials; tuned
bulwahn [Wed, 10 Oct 2012 10:41:16 +0200] rev 49761
set_comprehension_pointfree also handles terms where the equation is not at the first position, which is a necessary generalisation to eventually handle bounded existentials; tuned
Wed, 10 Oct 2012 08:45:27 +0200 more consistent error messages on malformed code equations
haftmann [Wed, 10 Oct 2012 08:45:27 +0200] rev 49760
more consistent error messages on malformed code equations
Tue, 09 Oct 2012 17:33:46 +0200 removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman [Tue, 09 Oct 2012 17:33:46 +0200] rev 49759
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands; removed '(open)', '(set_name)' and '(open set_name)' options
Tue, 09 Oct 2012 16:58:36 +0200 use Set.filter instead of Finite_Set.filter, which is removed then
kuncar [Tue, 09 Oct 2012 16:58:36 +0200] rev 49758
use Set.filter instead of Finite_Set.filter, which is removed then
Tue, 09 Oct 2012 16:57:58 +0200 rename Set.project to Set.filter - more appropriate name
kuncar [Tue, 09 Oct 2012 16:57:58 +0200] rev 49757
rename Set.project to Set.filter - more appropriate name
Wed, 10 Oct 2012 15:39:01 +0200 added some ad-hoc namespace prefixes to avoid duplicate facts;
wenzelm [Wed, 10 Oct 2012 15:39:01 +0200] rev 49756
added some ad-hoc namespace prefixes to avoid duplicate facts;
Wed, 10 Oct 2012 15:27:10 +0200 avoid duplicate facts;
wenzelm [Wed, 10 Oct 2012 15:27:10 +0200] rev 49755
avoid duplicate facts;
Wed, 10 Oct 2012 15:21:26 +0200 more explicit namespace prefix for 'statespace' -- duplicate facts;
wenzelm [Wed, 10 Oct 2012 15:21:26 +0200] rev 49754
more explicit namespace prefix for 'statespace' -- duplicate facts;
Wed, 10 Oct 2012 15:17:40 +0200 eliminated spurious fact duplicates;
wenzelm [Wed, 10 Oct 2012 15:17:40 +0200] rev 49753
eliminated spurious fact duplicates;
Wed, 10 Oct 2012 15:01:20 +0200 modernized dynamic "rules" -- avoid rebinding of static facts;
wenzelm [Wed, 10 Oct 2012 15:01:20 +0200] rev 49752
modernized dynamic "rules" -- avoid rebinding of static facts;
Tue, 09 Oct 2012 22:24:24 +0200 removed redundant lemma, cf. class zero_neq_one in HOL/Rings.thy;
wenzelm [Tue, 09 Oct 2012 22:24:24 +0200] rev 49751
removed redundant lemma, cf. class zero_neq_one in HOL/Rings.thy;
Tue, 09 Oct 2012 21:33:12 +0200 clarified Element.init vs. Element.activate: refrain from hard-wiring Thm.def_binding_optional to avoid duplicate facts;
wenzelm [Tue, 09 Oct 2012 21:33:12 +0200] rev 49750
clarified Element.init vs. Element.activate: refrain from hard-wiring Thm.def_binding_optional to avoid duplicate facts;
Tue, 09 Oct 2012 20:23:58 +0200 tuned;
wenzelm [Tue, 09 Oct 2012 20:23:58 +0200] rev 49749
tuned;
Tue, 09 Oct 2012 20:05:17 +0200 clarified Local_Defs.add_def(s): refrain from hard-wiring Thm.def_binding_optional;
wenzelm [Tue, 09 Oct 2012 20:05:17 +0200] rev 49748
clarified Local_Defs.add_def(s): refrain from hard-wiring Thm.def_binding_optional; clarified Generic_Target.define: avoid duplicate def binding via Local_Defs.add_def;
Tue, 09 Oct 2012 19:24:19 +0200 more explicit flags for facts table;
wenzelm [Tue, 09 Oct 2012 19:24:19 +0200] rev 49747
more explicit flags for facts table;
Tue, 09 Oct 2012 15:31:45 +0200 minor tuning;
wenzelm [Tue, 09 Oct 2012 15:31:45 +0200] rev 49746
minor tuning;
Tue, 09 Oct 2012 13:57:51 +0200 more conventional Double constants;
wenzelm [Tue, 09 Oct 2012 13:57:51 +0200] rev 49745
more conventional Double constants;
Tue, 09 Oct 2012 13:50:24 +0200 tuned source structure;
wenzelm [Tue, 09 Oct 2012 13:50:24 +0200] rev 49744
tuned source structure;
Tue, 09 Oct 2012 13:29:43 +0200 tuned;
wenzelm [Tue, 09 Oct 2012 13:29:43 +0200] rev 49743
tuned;
Tue, 09 Oct 2012 13:27:52 +0200 tuned;
wenzelm [Tue, 09 Oct 2012 13:27:52 +0200] rev 49742
tuned;
Tue, 09 Oct 2012 11:51:06 +0200 merged
wenzelm [Tue, 09 Oct 2012 11:51:06 +0200] rev 49741
merged
Tue, 09 Oct 2012 00:40:33 +0200 added type annotations to generated Isar proofs -- code by Steffen Smolka
blanchet [Tue, 09 Oct 2012 00:40:33 +0200] rev 49740
added type annotations to generated Isar proofs -- code by Steffen Smolka
Mon, 08 Oct 2012 12:03:49 +0200 consolidated names of theorems on composition;
haftmann [Mon, 08 Oct 2012 12:03:49 +0200] rev 49739
consolidated names of theorems on composition; generalized former theorem UN_o; comp_assoc orients to the right, as is more common
Mon, 08 Oct 2012 11:37:03 +0200 corrected NEWS
haftmann [Mon, 08 Oct 2012 11:37:03 +0200] rev 49738
corrected NEWS
Mon, 08 Oct 2012 23:29:07 +0200 avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm [Mon, 08 Oct 2012 23:29:07 +0200] rev 49737
avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient; more elementary level_list: avoid stack overflow; prefer elementary graph operations; tuned;
Mon, 08 Oct 2012 21:17:20 +0200 clarified long_names -- conform to usual Isabelle practice of not analysing internal names;
wenzelm [Mon, 08 Oct 2012 21:17:20 +0200] rev 49736
clarified long_names -- conform to usual Isabelle practice of not analysing internal names;
Mon, 08 Oct 2012 20:39:57 +0200 more precise repaint and revalidate -- the latter is important to keep in sync with content update;
wenzelm [Mon, 08 Oct 2012 20:39:57 +0200] rev 49735
more precise repaint and revalidate -- the latter is important to keep in sync with content update;
Mon, 08 Oct 2012 14:49:04 +0200 tuned;
wenzelm [Mon, 08 Oct 2012 14:49:04 +0200] rev 49734
tuned;
Mon, 08 Oct 2012 14:10:38 +0200 prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm [Mon, 08 Oct 2012 14:10:38 +0200] rev 49733
prefer synchronous Mutator_Event.Bus on Swing_Thread;
Mon, 08 Oct 2012 13:20:55 +0200 more direct tooltip content;
wenzelm [Mon, 08 Oct 2012 13:20:55 +0200] rev 49732
more direct tooltip content;
Mon, 08 Oct 2012 12:54:00 +0200 tuned;
wenzelm [Mon, 08 Oct 2012 12:54:00 +0200] rev 49731
tuned;
Mon, 08 Oct 2012 12:40:35 +0200 use Pretty_Tooltip for Graphview_Panel;
wenzelm [Mon, 08 Oct 2012 12:40:35 +0200] rev 49730
use Pretty_Tooltip for Graphview_Panel; tuned signature;
Mon, 08 Oct 2012 12:02:32 +0200 more basic tooltips;
wenzelm [Mon, 08 Oct 2012 12:02:32 +0200] rev 49729
more basic tooltips;
Sun, 07 Oct 2012 16:26:31 +0200 close tooltips more thoroughly;
wenzelm [Sun, 07 Oct 2012 16:26:31 +0200] rev 49728
close tooltips more thoroughly;
Sun, 07 Oct 2012 16:15:31 +0200 make buttons closer to original mouse position;
wenzelm [Sun, 07 Oct 2012 16:15:31 +0200] rev 49727
make buttons closer to original mouse position;
Sun, 07 Oct 2012 16:05:31 +0200 detach tooltip as dockable window;
wenzelm [Sun, 07 Oct 2012 16:05:31 +0200] rev 49726
detach tooltip as dockable window;
Sun, 07 Oct 2012 15:05:11 +0200 explicit close button;
wenzelm [Sun, 07 Oct 2012 15:05:11 +0200] rev 49725
explicit close button;
Sat, 06 Oct 2012 16:03:41 +0200 congruence rule for Finite_Set.fold
haftmann [Sat, 06 Oct 2012 16:03:41 +0200] rev 49724
congruence rule for Finite_Set.fold
Sat, 06 Oct 2012 11:08:52 +0200 alternative simplification of ^^ to the righthand side;
haftmann [Sat, 06 Oct 2012 11:08:52 +0200] rev 49723
alternative simplification of ^^ to the righthand side; lifting of comp_fun_commute to ^^
Fri, 05 Oct 2012 18:01:48 +0200 eliminated obsolete tooltip delay -- bypassed by Pretty_Tooltip;
wenzelm [Fri, 05 Oct 2012 18:01:48 +0200] rev 49722
eliminated obsolete tooltip delay -- bypassed by Pretty_Tooltip;
Fri, 05 Oct 2012 14:51:33 +0200 merged
wenzelm [Fri, 05 Oct 2012 14:51:33 +0200] rev 49721
merged
Fri, 05 Oct 2012 10:57:03 +0200 newer versions of Z3 call it "Bool" not "bool"
blanchet [Fri, 05 Oct 2012 10:57:03 +0200] rev 49720
newer versions of Z3 call it "Bool" not "bool"
Thu, 04 Oct 2012 23:19:02 +0200 simplified type of msetprod;
haftmann [Thu, 04 Oct 2012 23:19:02 +0200] rev 49719
simplified type of msetprod; n.b. image function need not be part of minimal definition of msetprod, since multisets may already contain repeated elements
Thu, 04 Oct 2012 23:19:02 +0200 tuned proof
haftmann [Thu, 04 Oct 2012 23:19:02 +0200] rev 49718
tuned proof
Thu, 04 Oct 2012 23:19:02 +0200 default simp rule for image under identity
haftmann [Thu, 04 Oct 2012 23:19:02 +0200] rev 49717
default simp rule for image under identity
Thu, 04 Oct 2012 23:19:02 +0200 dropped duplicate facts; tuned syntax
haftmann [Thu, 04 Oct 2012 23:19:02 +0200] rev 49716
dropped duplicate facts; tuned syntax
Thu, 04 Oct 2012 23:19:02 +0200 more facts on setsum and setprod
haftmann [Thu, 04 Oct 2012 23:19:02 +0200] rev 49715
more facts on setsum and setprod
Thu, 04 Oct 2012 17:26:04 +0200 made SML/NJ happier
traytel [Thu, 04 Oct 2012 17:26:04 +0200] rev 49714
made SML/NJ happier
Thu, 04 Oct 2012 17:16:55 +0200 do not expose details of internal data structures for composition of BNFs
traytel [Thu, 04 Oct 2012 17:16:55 +0200] rev 49713
do not expose details of internal data structures for composition of BNFs
Fri, 05 Oct 2012 14:32:56 +0200 further support for nested tooltips;
wenzelm [Fri, 05 Oct 2012 14:32:56 +0200] rev 49712
further support for nested tooltips;
Fri, 05 Oct 2012 13:57:48 +0200 tuned proofs;
wenzelm [Fri, 05 Oct 2012 13:57:48 +0200] rev 49711
tuned proofs;
Fri, 05 Oct 2012 13:48:22 +0200 refer to parent frame -- relevant for floating dockables in particular;
wenzelm [Fri, 05 Oct 2012 13:48:22 +0200] rev 49710
refer to parent frame -- relevant for floating dockables in particular;
Fri, 05 Oct 2012 12:11:23 +0200 tuned window position to fit on screen;
wenzelm [Fri, 05 Oct 2012 12:11:23 +0200] rev 49709
tuned window position to fit on screen;
Fri, 05 Oct 2012 12:00:28 +0200 tuned window position;
wenzelm [Fri, 05 Oct 2012 12:00:28 +0200] rev 49708
tuned window position;
Fri, 05 Oct 2012 11:36:46 +0200 determine window size from content;
wenzelm [Fri, 05 Oct 2012 11:36:46 +0200] rev 49707
determine window size from content;
Fri, 05 Oct 2012 11:09:24 +0200 tuned color and font size;
wenzelm [Fri, 05 Oct 2012 11:09:24 +0200] rev 49706
tuned color and font size;
Fri, 05 Oct 2012 10:54:07 +0200 close tooltip window on escape;
wenzelm [Fri, 05 Oct 2012 10:54:07 +0200] rev 49705
close tooltip window on escape; tuned;
Fri, 05 Oct 2012 10:23:49 +0200 proper message markup for output;
wenzelm [Fri, 05 Oct 2012 10:23:49 +0200] rev 49704
proper message markup for output;
Thu, 04 Oct 2012 20:36:10 +0200 some re-ordering of initialization to ensure proper formatting;
wenzelm [Thu, 04 Oct 2012 20:36:10 +0200] rev 49703
some re-ordering of initialization to ensure proper formatting;
Thu, 04 Oct 2012 20:14:40 +0200 separate module Pretty_Tooltip;
wenzelm [Thu, 04 Oct 2012 20:14:40 +0200] rev 49702
separate module Pretty_Tooltip;
Thu, 04 Oct 2012 19:31:50 +0200 refined rich tooltip options;
wenzelm [Thu, 04 Oct 2012 19:31:50 +0200] rev 49701
refined rich tooltip options; basic tooltips without markup;
Thu, 04 Oct 2012 18:28:31 +0200 Rich_Text_Area tooltips via nested Pretty_Text_Area, based on some techniques of FoldViewer plugin;
wenzelm [Thu, 04 Oct 2012 18:28:31 +0200] rev 49700
Rich_Text_Area tooltips via nested Pretty_Text_Area, based on some techniques of FoldViewer plugin;
Thu, 04 Oct 2012 13:56:32 +0200 some documentation of show_markup;
wenzelm [Thu, 04 Oct 2012 13:56:32 +0200] rev 49699
some documentation of show_markup;
Thu, 04 Oct 2012 11:45:56 +0200 tuned proofs;
wenzelm [Thu, 04 Oct 2012 11:45:56 +0200] rev 49698
tuned proofs;
Thu, 04 Oct 2012 11:39:24 +0200 option to bypass potentially slow text overview;
wenzelm [Thu, 04 Oct 2012 11:39:24 +0200] rev 49697
option to bypass potentially slow text overview;
Thu, 04 Oct 2012 11:07:36 +0200 tuned signature;
wenzelm [Thu, 04 Oct 2012 11:07:36 +0200] rev 49696
tuned signature;
Thu, 04 Oct 2012 10:55:36 +0200 clarified platform dependency;
wenzelm [Thu, 04 Oct 2012 10:55:36 +0200] rev 49695
clarified platform dependency;
Thu, 04 Oct 2012 09:19:54 +1000 updated crontab and afp-poly settings
Gerwin Klein <gerwin.klein@nicta.com.au> [Thu, 04 Oct 2012 09:19:54 +1000] rev 49694
updated crontab and afp-poly settings
Wed, 03 Oct 2012 22:07:26 +0200 thread the right local theory through + reenable parallel proofs for previously problematic theories
blanchet [Wed, 03 Oct 2012 22:07:26 +0200] rev 49693
thread the right local theory through + reenable parallel proofs for previously problematic theories
Wed, 03 Oct 2012 21:46:52 +0200 made code more conform to rest of BNF package
blanchet [Wed, 03 Oct 2012 21:46:52 +0200] rev 49692
made code more conform to rest of BNF package
Wed, 03 Oct 2012 17:12:08 +0200 more error positions;
wenzelm [Wed, 03 Oct 2012 17:12:08 +0200] rev 49691
more error positions;
Wed, 03 Oct 2012 16:59:58 +0200 more explicit show_type_constraint, show_sort_constraint;
wenzelm [Wed, 03 Oct 2012 16:59:58 +0200] rev 49690
more explicit show_type_constraint, show_sort_constraint;
Wed, 03 Oct 2012 16:59:20 +0200 recovered print translation after 'a => bool to 'a set change;
wenzelm [Wed, 03 Oct 2012 16:59:20 +0200] rev 49689
recovered print translation after 'a => bool to 'a set change;
Wed, 03 Oct 2012 16:43:41 +0200 tuned;
wenzelm [Wed, 03 Oct 2012 16:43:41 +0200] rev 49688
tuned;
Wed, 03 Oct 2012 16:42:36 +0200 use explicit Type.strip_sorts_dummy to suppress sort constraints in output;
wenzelm [Wed, 03 Oct 2012 16:42:36 +0200] rev 49687
use explicit Type.strip_sorts_dummy to suppress sort constraints in output;
Wed, 03 Oct 2012 16:01:07 +0200 printed "_ofsort" is subject to show_markup as well;
wenzelm [Wed, 03 Oct 2012 16:01:07 +0200] rev 49686
printed "_ofsort" is subject to show_markup as well;
Wed, 03 Oct 2012 14:58:56 +0200 allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm [Wed, 03 Oct 2012 14:58:56 +0200] rev 49685
allow position constraints to coexist with 0 or 1 sort constraints; more position information in sorting error; report sorting of all type variables;
Tue, 02 Oct 2012 09:20:28 +0200 made tactic more robust (less usage of stac)
traytel [Tue, 02 Oct 2012 09:20:28 +0200] rev 49684
made tactic more robust (less usage of stac)
Tue, 02 Oct 2012 01:00:18 +0200 continued changing type of corec type
blanchet [Tue, 02 Oct 2012 01:00:18 +0200] rev 49683
continued changing type of corec type
Tue, 02 Oct 2012 01:00:18 +0200 removed dead params and dead code
blanchet [Tue, 02 Oct 2012 01:00:18 +0200] rev 49682
removed dead params and dead code
Tue, 02 Oct 2012 01:00:18 +0200 changed type of corecursor for the nested recursion case
blanchet [Tue, 02 Oct 2012 01:00:18 +0200] rev 49681
changed type of corecursor for the nested recursion case
Tue, 02 Oct 2012 01:00:18 +0200 made (co)rec tactic more robust when the simplifier succeeds early
blanchet [Tue, 02 Oct 2012 01:00:18 +0200] rev 49680
made (co)rec tactic more robust when the simplifier succeeds early
Mon, 01 Oct 2012 20:38:57 +0200 tuned;
wenzelm [Mon, 01 Oct 2012 20:38:57 +0200] rev 49679
tuned;
Mon, 01 Oct 2012 20:35:09 +0200 removed unused module Blob;
wenzelm [Mon, 01 Oct 2012 20:35:09 +0200] rev 49678
removed unused module Blob;
Mon, 01 Oct 2012 20:17:30 +0200 more direct message header: eliminated historic encoding via single letter;
wenzelm [Mon, 01 Oct 2012 20:17:30 +0200] rev 49677
more direct message header: eliminated historic encoding via single letter;
Mon, 01 Oct 2012 20:16:37 +0200 tuned whitespace;
wenzelm [Mon, 01 Oct 2012 20:16:37 +0200] rev 49676
tuned whitespace;
Mon, 01 Oct 2012 17:29:00 +0200 tuned proofs;
wenzelm [Mon, 01 Oct 2012 17:29:00 +0200] rev 49675
tuned proofs;
Mon, 01 Oct 2012 16:37:22 +0200 report sort assignment of visible type variables;
wenzelm [Mon, 01 Oct 2012 16:37:22 +0200] rev 49674
report sort assignment of visible type variables;
Mon, 01 Oct 2012 12:05:05 +0200 more robust File.eq, and thus File.copy of "~~/lib/logo/isabelle.gif";
wenzelm [Mon, 01 Oct 2012 12:05:05 +0200] rev 49673
more robust File.eq, and thus File.copy of "~~/lib/logo/isabelle.gif";
Mon, 01 Oct 2012 11:04:30 +0200 fixed recursor definition for datatypes with inner products (e.g. "'a trm" from the lambda-term example)
blanchet [Mon, 01 Oct 2012 11:04:30 +0200] rev 49672
fixed recursor definition for datatypes with inner products (e.g. "'a trm" from the lambda-term example)
Mon, 01 Oct 2012 10:46:30 +0200 tweaked corecursor/coiterator tactic
blanchet [Mon, 01 Oct 2012 10:46:30 +0200] rev 49671
tweaked corecursor/coiterator tactic
Mon, 01 Oct 2012 10:34:58 +0200 changed the type of the recursor for nested recursion
blanchet [Mon, 01 Oct 2012 10:34:58 +0200] rev 49670
changed the type of the recursor for nested recursion
(0) -30000 -10000 -3000 -1000 -120 +120 +1000 +3000 +10000 +30000 tip