2010-01-13 Removed the 'oops' in IntEx.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 13 Jan 2010 13:12:04 +0100] rev 859
Removed the 'oops' in IntEx.
2010-01-13 tuned
Christian Urban <urbanc@in.tum.de> [Wed, 13 Jan 2010 09:41:57 +0100] rev 858
tuned
2010-01-13 added SOLVED' which is now part of Isabelle....must be removed eventually
Christian Urban <urbanc@in.tum.de> [Wed, 13 Jan 2010 09:30:59 +0100] rev 857
added SOLVED' which is now part of Isabelle....must be removed eventually
2010-01-13 merged
Christian Urban <urbanc@in.tum.de> [Wed, 13 Jan 2010 09:19:20 +0100] rev 856
merged
2010-01-12 tuned
Christian Urban <urbanc@in.tum.de> [Wed, 13 Jan 2010 00:46:31 +0100] rev 855
tuned
2010-01-12 absrep_fun and equiv_relation do not produce anymore spurious maps; two problems arose in IntEx, which are marked with "INJECTION PROBLEM"
Christian Urban <urbanc@in.tum.de> [Wed, 13 Jan 2010 00:45:28 +0100] rev 854
absrep_fun and equiv_relation do not produce anymore spurious maps; two problems arose in IntEx, which are marked with "INJECTION PROBLEM"
2010-01-12 More indenting, bracket removing and comment restructuring.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 12 Jan 2010 17:46:35 +0100] rev 853
More indenting, bracket removing and comment restructuring.
2010-01-12 Finished replacing OO by OOO
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 12 Jan 2010 16:44:33 +0100] rev 852
Finished replacing OO by OOO
2010-01-12 Change OO to OOO in FSet3.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 12 Jan 2010 16:28:53 +0100] rev 851
Change OO to OOO in FSet3.
2010-01-12 minor comment editing
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 12 Jan 2010 16:21:42 +0100] rev 850
minor comment editing
2010-01-12 modifying comments/indentation in quotient_term.ml
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 12 Jan 2010 16:12:54 +0100] rev 849
modifying comments/indentation in quotient_term.ml
2010-01-12 Cleaning comments, indentation etc in quotient_tacs.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 12 Jan 2010 16:03:51 +0100] rev 848
Cleaning comments, indentation etc in quotient_tacs.
2010-01-12 No more exception handling in rep_abs_rsp_tac
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 12 Jan 2010 15:48:46 +0100] rev 847
No more exception handling in rep_abs_rsp_tac
2010-01-12 handle all is no longer necessary in lambda_prs.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 12 Jan 2010 12:14:33 +0100] rev 846
handle all is no longer necessary in lambda_prs.
2010-01-12 removed 3 hacks.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 12 Jan 2010 12:04:47 +0100] rev 845
removed 3 hacks.
2010-01-12 Updated some comments.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 12 Jan 2010 11:25:38 +0100] rev 844
Updated some comments.
2010-01-12 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 12 Jan 2010 10:59:51 +0100] rev 843
merge
2010-01-12 Removed exception handling from equals_rsp_tac.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 12 Jan 2010 10:59:38 +0100] rev 842
Removed exception handling from equals_rsp_tac.
2010-01-11 added an abbreviation for OOO
Christian Urban <urbanc@in.tum.de> [Mon, 11 Jan 2010 22:36:21 +0100] rev 841
added an abbreviation for OOO
2010-01-11 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 11 Jan 2010 20:04:19 +0100] rev 840
merge
2010-01-11 Undid the non-working part.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 11 Jan 2010 20:03:43 +0100] rev 839
Undid the non-working part.
2010-01-11 started to adhere to Wenzel-Standard
Christian Urban <urbanc@in.tum.de> [Mon, 11 Jan 2010 16:33:00 +0100] rev 838
started to adhere to Wenzel-Standard
2010-01-11 Changing exceptions to 'try', part 1.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 11 Jan 2010 15:58:38 +0100] rev 837
Changing exceptions to 'try', part 1.
2010-01-11 removed quotdata_lookup_type
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 11 Jan 2010 15:13:09 +0100] rev 836
removed quotdata_lookup_type
2010-01-11 Fix for testing matching constants in regularize.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 11 Jan 2010 11:51:19 +0100] rev 835
Fix for testing matching constants in regularize.
2010-01-11 tuned previous commit further
Christian Urban <urbanc@in.tum.de> [Mon, 11 Jan 2010 01:03:34 +0100] rev 834
tuned previous commit further
2010-01-10 the chk-functions in quotient_term also simplify the result according to the id_simps; had to remove id_def from this theorem list though; this caused in FSet3 that relied on this rule; the problem is marked with "ID PROBLEM"
Christian Urban <urbanc@in.tum.de> [Mon, 11 Jan 2010 00:31:29 +0100] rev 833
the chk-functions in quotient_term also simplify the result according to the id_simps; had to remove id_def from this theorem list though; this caused in FSet3 that relied on this rule; the problem is marked with "ID PROBLEM"
2010-01-09 introduced separate match function
Christian Urban <urbanc@in.tum.de> [Sat, 09 Jan 2010 09:38:34 +0100] rev 832
introduced separate match function
2010-01-09 removed obsolete equiv_relation and rnamed new_equiv_relation
Christian Urban <urbanc@in.tum.de> [Sat, 09 Jan 2010 08:52:06 +0100] rev 831
removed obsolete equiv_relation and rnamed new_equiv_relation
2010-01-08 New_relations, all works again including concat examples.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 08 Jan 2010 19:46:22 +0100] rev 830
New_relations, all works again including concat examples.
2010-01-08 map and rel simps for all quotients; needed when changing the relations to aggregate ones.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 08 Jan 2010 15:02:12 +0100] rev 829
map and rel simps for all quotients; needed when changing the relations to aggregate ones.
2010-01-08 id_simps needs to be taken out not used directly, otherwise the new lemmas are not there.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 08 Jan 2010 14:43:30 +0100] rev 828
id_simps needs to be taken out not used directly, otherwise the new lemmas are not there.
2010-01-08 Experimients with fconcat_insert
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 08 Jan 2010 11:20:12 +0100] rev 827
Experimients with fconcat_insert
2010-01-08 Modifications for new_equiv_rel, part2
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 08 Jan 2010 10:44:30 +0100] rev 826
Modifications for new_equiv_rel, part2
2010-01-08 Modifictaions for new_relation.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 08 Jan 2010 10:39:08 +0100] rev 825
Modifictaions for new_relation.
2010-01-08 Proved concat_empty.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 08 Jan 2010 10:08:01 +0100] rev 824
Proved concat_empty.
2010-01-07 Replacing equivp by reflp in the assumptions leads to non-provable subgoals in the gen_pre lemmas.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 07 Jan 2010 16:51:38 +0100] rev 823
Replacing equivp by reflp in the assumptions leads to non-provable subgoals in the gen_pre lemmas.
2010-01-07 some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 07 Jan 2010 16:06:13 +0100] rev 822
some cleaning.
2010-01-07 First generalization.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 07 Jan 2010 15:50:22 +0100] rev 821
First generalization.
2010-01-07 The working proof of the special case.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 07 Jan 2010 14:14:17 +0100] rev 820
The working proof of the special case.
2010-01-07 Reduced the proof to two simple but not obvious to prove facts.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 07 Jan 2010 10:55:20 +0100] rev 819
Reduced the proof to two simple but not obvious to prove facts.
2010-01-07 More cleaning and commenting AbsRepTest. Now tests work; just slow.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 07 Jan 2010 10:13:15 +0100] rev 818
More cleaning and commenting AbsRepTest. Now tests work; just slow.
2010-01-07 cleaning in AbsRepTest.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 07 Jan 2010 09:55:42 +0100] rev 817
cleaning in AbsRepTest.
2010-01-06 Further in the proof
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 06 Jan 2010 16:24:21 +0100] rev 816
Further in the proof
2010-01-06 Tried to prove the lemma manually; only left with quotient proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 06 Jan 2010 09:19:23 +0100] rev 815
Tried to prove the lemma manually; only left with quotient proofs.
2010-01-06 Sledgehammer bug.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 06 Jan 2010 08:24:37 +0100] rev 814
Sledgehammer bug.
2010-01-05 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 05 Jan 2010 18:10:20 +0100] rev 813
merge
2010-01-05 Trying the proof
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 05 Jan 2010 18:09:03 +0100] rev 812
Trying the proof
2010-01-05 merged
Christian Urban <urbanc@in.tum.de> [Tue, 05 Jan 2010 17:12:35 +0100] rev 811
merged
2010-01-05 Struggling with composition
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 05 Jan 2010 17:06:51 +0100] rev 810
Struggling with composition
2010-01-05 Trying to state composition quotient.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 05 Jan 2010 15:25:31 +0100] rev 809
Trying to state composition quotient.
2010-01-05 proper handling of error messages (code copy - maybe this can be avoided)
Christian Urban <urbanc@in.tum.de> [Tue, 05 Jan 2010 14:23:45 +0100] rev 808
proper handling of error messages (code copy - maybe this can be avoided)
2010-01-05 added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de> [Tue, 05 Jan 2010 14:09:04 +0100] rev 807
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
2010-01-05 Readded 'regularize_to_injection' which I believe will be needed.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 05 Jan 2010 10:41:20 +0100] rev 806
Readded 'regularize_to_injection' which I believe will be needed.
2010-01-02 added a warning to the quotient_type definition, if a map function is missing
Christian Urban <urbanc@in.tum.de> [Sat, 02 Jan 2010 23:15:15 +0100] rev 805
added a warning to the quotient_type definition, if a map function is missing
2010-01-01 tuned
Christian Urban <urbanc@in.tum.de> [Fri, 01 Jan 2010 23:59:32 +0100] rev 804
tuned
2010-01-01 a slight change to abs/rep generation
Christian Urban <urbanc@in.tum.de> [Fri, 01 Jan 2010 11:30:00 +0100] rev 803
a slight change to abs/rep generation
2010-01-01 tuned
Christian Urban <urbanc@in.tum.de> [Fri, 01 Jan 2010 04:39:43 +0100] rev 802
tuned
2010-01-01 fixed comment errors
Christian Urban <urbanc@in.tum.de> [Fri, 01 Jan 2010 01:10:38 +0100] rev 801
fixed comment errors
2010-01-01 some slight tuning
Christian Urban <urbanc@in.tum.de> [Fri, 01 Jan 2010 01:08:19 +0100] rev 800
some slight tuning
2009-12-31 renamed transfer to transform (Markus)
Christian Urban <urbanc@in.tum.de> [Thu, 31 Dec 2009 23:53:10 +0100] rev 799
renamed transfer to transform (Markus)
2009-12-30 some small changes
cu@localhost [Wed, 30 Dec 2009 12:10:57 +0000] rev 798
some small changes
2009-12-27 added a functor that allows checking what is added to the theorem lists
Christian Urban <urbanc@in.tum.de> [Sun, 27 Dec 2009 23:33:10 +0100] rev 797
added a functor that allows checking what is added to the theorem lists
2009-12-26 corrected wrong [quot_respect] attribute; tuned
Christian Urban <urbanc@in.tum.de> [Sat, 26 Dec 2009 23:20:46 +0100] rev 796
corrected wrong [quot_respect] attribute; tuned
2009-12-26 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de> [Sat, 26 Dec 2009 21:36:20 +0100] rev 795
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
2009-12-26 added an item about when the same quotient constant is defined twice (throws a bind exception in quoteint_def.ML)
Christian Urban <urbanc@in.tum.de> [Sat, 26 Dec 2009 20:45:37 +0100] rev 794
added an item about when the same quotient constant is defined twice (throws a bind exception in quoteint_def.ML)
2009-12-26 as expected problems occure when lifting concat lemmas
Christian Urban <urbanc@in.tum.de> [Sat, 26 Dec 2009 20:24:53 +0100] rev 793
as expected problems occure when lifting concat lemmas
2009-12-26 tuned
Christian Urban <urbanc@in.tum.de> [Sat, 26 Dec 2009 09:03:35 +0100] rev 792
tuned
2009-12-26 commeted the absrep function
Christian Urban <urbanc@in.tum.de> [Sat, 26 Dec 2009 08:06:45 +0100] rev 791
commeted the absrep function
2009-12-26 generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de> [Sat, 26 Dec 2009 07:15:30 +0100] rev 790
generalised absrep function; needs consolidation
2009-12-24 tuned
Christian Urban <urbanc@in.tum.de> [Fri, 25 Dec 2009 00:58:06 +0100] rev 789
tuned
2009-12-24 added sanity checks for quotient_type
Christian Urban <urbanc@in.tum.de> [Fri, 25 Dec 2009 00:17:55 +0100] rev 788
added sanity checks for quotient_type
2009-12-24 made the quotient_type definition more like typedef; now type variables need to be explicitly given
Christian Urban <urbanc@in.tum.de> [Thu, 24 Dec 2009 22:28:19 +0100] rev 787
made the quotient_type definition more like typedef; now type variables need to be explicitly given
2009-12-23 used Local_Theory.declaration for storing quotdata
Christian Urban <urbanc@in.tum.de> [Thu, 24 Dec 2009 00:58:50 +0100] rev 786
used Local_Theory.declaration for storing quotdata
2009-12-23 tuning
Christian Urban <urbanc@in.tum.de> [Wed, 23 Dec 2009 23:53:03 +0100] rev 785
tuning
2009-12-23 renamed some fields in the info records
Christian Urban <urbanc@in.tum.de> [Wed, 23 Dec 2009 23:22:02 +0100] rev 784
renamed some fields in the info records
2009-12-23 modified mk_resp_arg so that the user can give terms as equivalence relations, not just constants
Christian Urban <urbanc@in.tum.de> [Wed, 23 Dec 2009 22:42:30 +0100] rev 783
modified mk_resp_arg so that the user can give terms as equivalence relations, not just constants
2009-12-23 cleaed a bit function mk_typedef_main
Christian Urban <urbanc@in.tum.de> [Wed, 23 Dec 2009 21:30:23 +0100] rev 782
cleaed a bit function mk_typedef_main
2009-12-23 renamed QUOT_TYPE to Quot_Type
Christian Urban <urbanc@in.tum.de> [Wed, 23 Dec 2009 13:45:42 +0100] rev 781
renamed QUOT_TYPE to Quot_Type
2009-12-23 explicit handling of mem_def, avoiding the use of the simplifier; this fixes some quotient_type definitions
Christian Urban <urbanc@in.tum.de> [Wed, 23 Dec 2009 13:23:33 +0100] rev 780
explicit handling of mem_def, avoiding the use of the simplifier; this fixes some quotient_type definitions
2009-12-23 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de> [Wed, 23 Dec 2009 10:31:54 +0100] rev 779
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
2009-12-22 added "Highest Priority" category; and tuned slightly code
Christian Urban <urbanc@in.tum.de> [Tue, 22 Dec 2009 22:10:48 +0100] rev 778
added "Highest Priority" category; and tuned slightly code
2009-12-22 added a print_maps command; updated the keyword file accordingly
Christian Urban <urbanc@in.tum.de> [Tue, 22 Dec 2009 21:44:50 +0100] rev 777
added a print_maps command; updated the keyword file accordingly
2009-12-22 renamed get_fun to absrep_fun; introduced explicit checked versions of the term functions
Christian Urban <urbanc@in.tum.de> [Tue, 22 Dec 2009 21:31:44 +0100] rev 776
renamed get_fun to absrep_fun; introduced explicit checked versions of the term functions
2009-12-22 tuned
Christian Urban <urbanc@in.tum.de> [Tue, 22 Dec 2009 21:16:11 +0100] rev 775
tuned
2009-12-22 moved get_fun into quotient_term; this simplifies the overall including structure of the package
Christian Urban <urbanc@in.tum.de> [Tue, 22 Dec 2009 21:06:46 +0100] rev 774
moved get_fun into quotient_term; this simplifies the overall including structure of the package
2009-12-22 tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de> [Tue, 22 Dec 2009 20:51:37 +0100] rev 773
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
2009-12-22 on the hunt for what condition raises which exception in the CLEVER CODE of calculate_inst
Christian Urban <urbanc@in.tum.de> [Tue, 22 Dec 2009 07:42:16 +0100] rev 772
on the hunt for what condition raises which exception in the CLEVER CODE of calculate_inst
2009-12-22 simplified calculate_instance; worked around some clever code; clever code is unfortunately still there...needs to be removed
Christian Urban <urbanc@in.tum.de> [Tue, 22 Dec 2009 07:28:09 +0100] rev 771
simplified calculate_instance; worked around some clever code; clever code is unfortunately still there...needs to be removed
2009-12-21 used eq_reflection not with OF, but directly in @{thm ...}
Christian Urban <urbanc@in.tum.de> [Mon, 21 Dec 2009 23:13:40 +0100] rev 770
used eq_reflection not with OF, but directly in @{thm ...}
2009-12-21 cleaned a bit calculate_inst a bit; eta-contraction seems to be not necessary? (all examples go through)
Christian Urban <urbanc@in.tum.de> [Mon, 21 Dec 2009 23:01:58 +0100] rev 769
cleaned a bit calculate_inst a bit; eta-contraction seems to be not necessary? (all examples go through)
2009-12-21 get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de> [Mon, 21 Dec 2009 22:36:31 +0100] rev 768
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
2009-12-19 on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de> [Sun, 20 Dec 2009 00:53:35 +0100] rev 767
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
2009-12-19 renamed "quotient" command to "quotient_type"; needs new keyword file to be installed
Christian Urban <urbanc@in.tum.de> [Sun, 20 Dec 2009 00:26:53 +0100] rev 766
renamed "quotient" command to "quotient_type"; needs new keyword file to be installed
2009-12-19 this file is now obsolete; replaced by isar-keywords-quot.el
Christian Urban <urbanc@in.tum.de> [Sun, 20 Dec 2009 00:15:40 +0100] rev 765
this file is now obsolete; replaced by isar-keywords-quot.el
2009-12-19 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place
Christian Urban <urbanc@in.tum.de> [Sun, 20 Dec 2009 00:14:46 +0100] rev 764
with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place
2009-12-19 added a very old paper about Quotients in Isabelle (related work)
Christian Urban <urbanc@in.tum.de> [Sat, 19 Dec 2009 22:42:31 +0100] rev 763
added a very old paper about Quotients in Isabelle (related work)
2009-12-19 avoided global "open"s - replaced by local "open"s
Christian Urban <urbanc@in.tum.de> [Sat, 19 Dec 2009 22:21:51 +0100] rev 762
avoided global "open"s - replaced by local "open"s
2009-12-19 small tuning
Christian Urban <urbanc@in.tum.de> [Sat, 19 Dec 2009 22:09:57 +0100] rev 761
small tuning
2009-12-19 various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de> [Sat, 19 Dec 2009 22:04:34 +0100] rev 760
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
2009-12-17 minor cleaning
Christian Urban <urbanc@in.tum.de> [Thu, 17 Dec 2009 17:59:12 +0100] rev 759
minor cleaning
2009-12-17 moved the QuotMain code into two ML-files
Christian Urban <urbanc@in.tum.de> [Thu, 17 Dec 2009 14:58:33 +0100] rev 758
moved the QuotMain code into two ML-files
2009-12-16 complete fix for IsaMakefile
Christian Urban <urbanc@in.tum.de> [Wed, 16 Dec 2009 14:28:48 +0100] rev 757
complete fix for IsaMakefile
2009-12-16 first fix
Christian Urban <urbanc@in.tum.de> [Wed, 16 Dec 2009 14:26:14 +0100] rev 756
first fix
2009-12-16 merged
Christian Urban <urbanc@in.tum.de> [Wed, 16 Dec 2009 14:09:03 +0100] rev 755
merged
2009-12-16 added a paper for possible notes
Christian Urban <urbanc@in.tum.de> [Wed, 16 Dec 2009 14:08:42 +0100] rev 754
added a paper for possible notes
2009-12-16 Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 16 Dec 2009 12:15:41 +0100] rev 753
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
2009-12-15 lambda_prs & solve_quotient_assum cleaned.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 15 Dec 2009 16:40:00 +0100] rev 752
lambda_prs & solve_quotient_assum cleaned.
2009-12-15 some commenting
Christian Urban <urbanc@in.tum.de> [Tue, 15 Dec 2009 15:38:17 +0100] rev 751
some commenting
2009-12-14 Fixed previous commit.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 14 Dec 2009 14:24:08 +0100] rev 750
Fixed previous commit.
2009-12-14 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 14 Dec 2009 13:59:08 +0100] rev 749
merge
2009-12-14 Moved DETERM inside Repeat & added SOLVE around quotient_tac.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 14 Dec 2009 13:58:51 +0100] rev 748
Moved DETERM inside Repeat & added SOLVE around quotient_tac.
2009-12-14 merge.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 14 Dec 2009 13:57:39 +0100] rev 747
merge.
2009-12-14 FIXME/TODO.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 14 Dec 2009 13:56:24 +0100] rev 746
FIXME/TODO.
2009-12-14 reply to question in code
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 14 Dec 2009 10:19:27 +0100] rev 745
reply to question in code
2009-12-14 Reply in code.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 14 Dec 2009 10:12:23 +0100] rev 744
Reply in code.
2009-12-14 Replies to questions from the weekend: Uncommenting the renamed theorem commented out in 734.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 14 Dec 2009 10:09:49 +0100] rev 743
Replies to questions from the weekend: Uncommenting the renamed theorem commented out in 734.
2009-12-13 a few code annotations
Christian Urban <urbanc@in.tum.de> [Sun, 13 Dec 2009 02:47:47 +0100] rev 742
a few code annotations
2009-12-13 another pass on apply_rsp
Christian Urban <urbanc@in.tum.de> [Sun, 13 Dec 2009 02:35:34 +0100] rev 741
another pass on apply_rsp
2009-12-13 managed to simplify apply_rsp
Christian Urban <urbanc@in.tum.de> [Sun, 13 Dec 2009 01:56:19 +0100] rev 740
managed to simplify apply_rsp
2009-12-12 tried to simplify apply_rsp_tac; failed at the moment; added some questions
Christian Urban <urbanc@in.tum.de> [Sat, 12 Dec 2009 18:43:42 +0100] rev 739
tried to simplify apply_rsp_tac; failed at the moment; added some questions
2009-12-12 some trivial changes
Christian Urban <urbanc@in.tum.de> [Sat, 12 Dec 2009 18:01:22 +0100] rev 738
some trivial changes
2009-12-12 trivial cleaning of make_inst
Christian Urban <urbanc@in.tum.de> [Sat, 12 Dec 2009 16:40:29 +0100] rev 737
trivial cleaning of make_inst
2009-12-12 tried to improve test; but fails
Christian Urban <urbanc@in.tum.de> [Sat, 12 Dec 2009 15:23:58 +0100] rev 736
tried to improve test; but fails
2009-12-12 merged
Christian Urban <urbanc@in.tum.de> [Sat, 12 Dec 2009 15:08:25 +0100] rev 735
merged
2009-12-12 annotated some questions to the code; some simple changes
Christian Urban <urbanc@in.tum.de> [Sat, 12 Dec 2009 15:07:59 +0100] rev 734
annotated some questions to the code; some simple changes
2009-12-12 Answering the question in code.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 12 Dec 2009 14:57:34 +0100] rev 733
Answering the question in code.
2009-12-12 merged
Christian Urban <urbanc@in.tum.de> [Sat, 12 Dec 2009 13:54:01 +0100] rev 732
merged
2009-12-12 trivial
Christian Urban <urbanc@in.tum.de> [Sat, 12 Dec 2009 13:53:46 +0100] rev 731
trivial
2009-12-12 tuned code
Christian Urban <urbanc@in.tum.de> [Sat, 12 Dec 2009 02:01:33 +0100] rev 730
tuned code
2009-12-12 Minor
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 12 Dec 2009 09:27:06 +0100] rev 729
Minor
2009-12-12 Some proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 12 Dec 2009 05:12:50 +0100] rev 728
Some proofs.
2009-12-12 Proof of finite_set_storng_cases_raw.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 12 Dec 2009 04:48:43 +0100] rev 727
Proof of finite_set_storng_cases_raw.
2009-12-12 A bracket was missing; with it proved the 'definitely false' lemma.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 12 Dec 2009 04:25:47 +0100] rev 726
A bracket was missing; with it proved the 'definitely false' lemma.
2009-12-12 renamed quotient.ML to quotient_typ.ML
Christian Urban <urbanc@in.tum.de> [Sat, 12 Dec 2009 01:44:56 +0100] rev 725
renamed quotient.ML to quotient_typ.ML
2009-12-11 merged
Christian Urban <urbanc@in.tum.de> [Fri, 11 Dec 2009 19:22:30 +0100] rev 724
merged
2009-12-11 tuned
Christian Urban <urbanc@in.tum.de> [Fri, 11 Dec 2009 19:19:50 +0100] rev 723
tuned
2009-12-11 started to have a look at it; redefined the relation
Christian Urban <urbanc@in.tum.de> [Fri, 11 Dec 2009 19:19:24 +0100] rev 722
started to have a look at it; redefined the relation
2009-12-11 More name and indentation cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 11 Dec 2009 17:59:29 +0100] rev 721
More name and indentation cleaning.
2009-12-11 Merge + Added LarryInt & Fset3 to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 11 Dec 2009 17:22:26 +0100] rev 720
Merge + Added LarryInt & Fset3 to tests.
2009-12-11 Renaming
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 11 Dec 2009 17:19:38 +0100] rev 719
Renaming
2009-12-11 merged
Christian Urban <urbanc@in.tum.de> [Fri, 11 Dec 2009 17:03:52 +0100] rev 718
merged
2009-12-11 deleted struct_match by Pattern.match (fixes a problem in LarryInt)
Christian Urban <urbanc@in.tum.de> [Fri, 11 Dec 2009 17:03:34 +0100] rev 717
deleted struct_match by Pattern.match (fixes a problem in LarryInt)
2009-12-11 FSet3 minor fixes + cases
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 11 Dec 2009 16:32:40 +0100] rev 716
FSet3 minor fixes + cases
2009-12-11 added Int example from Larry
Christian Urban <urbanc@in.tum.de> [Fri, 11 Dec 2009 15:58:15 +0100] rev 715
added Int example from Larry
2009-12-11 Added FSet3 with a formalisation of finite sets based on Michael's one.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 11 Dec 2009 15:49:15 +0100] rev 714
Added FSet3 with a formalisation of finite sets based on Michael's one.
2009-12-11 Updated TODO list together.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 11 Dec 2009 13:51:08 +0100] rev 713
Updated TODO list together.
2009-12-11 Merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 11 Dec 2009 11:32:29 +0100] rev 712
Merge
2009-12-11 More theorem renaming.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 11 Dec 2009 11:30:00 +0100] rev 711
More theorem renaming.
2009-12-11 Renamed theorems in IntEx2 to conform to names in Int.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 11 Dec 2009 11:25:52 +0100] rev 710
Renamed theorems in IntEx2 to conform to names in Int.
2009-12-11 Updated comments.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 11 Dec 2009 11:19:41 +0100] rev 709
Updated comments.
2009-12-11 merged
Christian Urban <urbanc@in.tum.de> [Fri, 11 Dec 2009 11:14:05 +0100] rev 708
merged
2009-12-11 tuned
Christian Urban <urbanc@in.tum.de> [Fri, 11 Dec 2009 11:12:53 +0100] rev 707
tuned
2009-12-11 renamed Larrys example
Christian Urban <urbanc@in.tum.de> [Fri, 11 Dec 2009 10:57:46 +0100] rev 706
renamed Larrys example
2009-12-11 New syntax for definitions.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 11 Dec 2009 11:08:58 +0100] rev 705
New syntax for definitions.
2009-12-11 changed error message
Christian Urban <urbanc@in.tum.de> [Fri, 11 Dec 2009 08:28:41 +0100] rev 704
changed error message
2009-12-11 reformulated the lemma lifting_procedure as ML value; gave better warning message for injection case
Christian Urban <urbanc@in.tum.de> [Fri, 11 Dec 2009 06:58:31 +0100] rev 703
reformulated the lemma lifting_procedure as ML value; gave better warning message for injection case
2009-12-10 slightly tuned
Christian Urban <urbanc@in.tum.de> [Thu, 10 Dec 2009 19:05:56 +0100] rev 702
slightly tuned
2009-12-10 merged
Christian Urban <urbanc@in.tum.de> [Thu, 10 Dec 2009 18:28:41 +0100] rev 701
merged
2009-12-10 added Larry's theory; introduced lemma equivpI; added something to the TODO about error messages
Christian Urban <urbanc@in.tum.de> [Thu, 10 Dec 2009 18:28:30 +0100] rev 700
added Larry's theory; introduced lemma equivpI; added something to the TODO about error messages
2009-12-10 added maps-printout and tuned some comments
Christian Urban <urbanc@in.tum.de> [Thu, 10 Dec 2009 16:56:03 +0100] rev 699
added maps-printout and tuned some comments
2009-12-10 Option and Sum quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 10 Dec 2009 14:35:06 +0100] rev 698
Option and Sum quotients.
2009-12-10 Regularized the hard lemma.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 10 Dec 2009 12:25:12 +0100] rev 697
Regularized the hard lemma.
2009-12-10 Simplification of Babses for regularize; will probably become injection
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 10 Dec 2009 11:19:34 +0100] rev 696
Simplification of Babses for regularize; will probably become injection
2009-12-10 Found the problem with ttt3.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 10 Dec 2009 10:54:45 +0100] rev 695
Found the problem with ttt3.
2009-12-10 minor
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 10 Dec 2009 10:36:05 +0100] rev 694
minor
2009-12-10 Moved Unused part of locale to Unused QuotMain.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 10 Dec 2009 10:21:51 +0100] rev 693
Moved Unused part of locale to Unused QuotMain.
2009-12-10 Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 10 Dec 2009 08:55:30 +0100] rev 692
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
2009-12-10 Removed 'Presburger' as it introduces int & other minor cleaning in Int2.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 10 Dec 2009 08:44:01 +0100] rev 691
Removed 'Presburger' as it introduces int & other minor cleaning in Int2.
2009-12-10 more tuning
Christian Urban <urbanc@in.tum.de> [Thu, 10 Dec 2009 05:11:53 +0100] rev 690
more tuning
2009-12-10 tuned
Christian Urban <urbanc@in.tum.de> [Thu, 10 Dec 2009 05:02:34 +0100] rev 689
tuned
2009-12-10 simplified the instantiation of QUOT_TRUE in procedure_tac
Christian Urban <urbanc@in.tum.de> [Thu, 10 Dec 2009 04:53:48 +0100] rev 688
simplified the instantiation of QUOT_TRUE in procedure_tac
2009-12-10 completed previous commit
Christian Urban <urbanc@in.tum.de> [Thu, 10 Dec 2009 04:35:08 +0100] rev 687
completed previous commit
2009-12-10 deleted DT/NDT diagnostic code
Christian Urban <urbanc@in.tum.de> [Thu, 10 Dec 2009 04:34:24 +0100] rev 686
deleted DT/NDT diagnostic code
2009-12-10 moved the interpretation code into Unused.thy
Christian Urban <urbanc@in.tum.de> [Thu, 10 Dec 2009 04:23:13 +0100] rev 685
moved the interpretation code into Unused.thy
2009-12-10 added an attempt to get a finite set theory
Christian Urban <urbanc@in.tum.de> [Thu, 10 Dec 2009 03:48:39 +0100] rev 684
added an attempt to get a finite set theory
2009-12-10 removed memb and used standard mem (member from List.thy)
Christian Urban <urbanc@in.tum.de> [Thu, 10 Dec 2009 03:47:10 +0100] rev 683
removed memb and used standard mem (member from List.thy)
2009-12-10 merged
Christian Urban <urbanc@in.tum.de> [Thu, 10 Dec 2009 03:25:42 +0100] rev 682
merged
2009-12-10 simplified proofs
Christian Urban <urbanc@in.tum.de> [Thu, 10 Dec 2009 03:11:19 +0100] rev 681
simplified proofs
2009-12-10 removed quot_respect attribute of a non-standard lemma
Christian Urban <urbanc@in.tum.de> [Thu, 10 Dec 2009 02:46:08 +0100] rev 680
removed quot_respect attribute of a non-standard lemma
2009-12-10 With int_of_nat as a quotient_def, lemmas about it can be easily lifted.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 10 Dec 2009 02:42:09 +0100] rev 679
With int_of_nat as a quotient_def, lemmas about it can be easily lifted.
2009-12-10 merged
Christian Urban <urbanc@in.tum.de> [Thu, 10 Dec 2009 01:48:39 +0100] rev 678
merged
2009-12-10 naming in this file cannot be made to agree to the original (PROBLEM?)
Christian Urban <urbanc@in.tum.de> [Thu, 10 Dec 2009 01:47:55 +0100] rev 677
naming in this file cannot be made to agree to the original (PROBLEM?)
2009-12-10 Lifted some kind of induction.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 10 Dec 2009 01:39:47 +0100] rev 676
Lifted some kind of induction.
2009-12-09 more proofs in IntEx2
Christian Urban <urbanc@in.tum.de> [Wed, 09 Dec 2009 23:32:16 +0100] rev 675
more proofs in IntEx2
2009-12-09 Finished one proof in IntEx2.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 09 Dec 2009 22:43:11 +0100] rev 674
Finished one proof in IntEx2.
2009-12-09 slightly more on IntEx2
Christian Urban <urbanc@in.tum.de> [Wed, 09 Dec 2009 22:05:11 +0100] rev 673
slightly more on IntEx2
2009-12-09 proved (with a lot of pain) that times_raw is respectful
Christian Urban <urbanc@in.tum.de> [Wed, 09 Dec 2009 20:35:52 +0100] rev 672
proved (with a lot of pain) that times_raw is respectful
2009-12-09 merged
Christian Urban <urbanc@in.tum.de> [Wed, 09 Dec 2009 17:31:19 +0100] rev 671
merged
2009-12-09 fixed minor stupidity
Christian Urban <urbanc@in.tum.de> [Wed, 09 Dec 2009 17:31:01 +0100] rev 670
fixed minor stupidity
2009-12-09 Exception handling.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 09 Dec 2009 17:16:39 +0100] rev 669
Exception handling.
2009-12-09 Code cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 09 Dec 2009 17:05:33 +0100] rev 668
Code cleaning.
2009-12-09 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 09 Dec 2009 16:44:34 +0100] rev 667
merge
2009-12-09 foldr_rsp.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 09 Dec 2009 16:43:12 +0100] rev 666
foldr_rsp.
2009-12-09 tuned
Christian Urban <urbanc@in.tum.de> [Wed, 09 Dec 2009 16:09:25 +0100] rev 665
tuned
2009-12-09 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 09 Dec 2009 15:59:02 +0100] rev 664
merge
2009-12-09 Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 09 Dec 2009 15:57:47 +0100] rev 663
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
2009-12-09 deleted make_inst3
Christian Urban <urbanc@in.tum.de> [Wed, 09 Dec 2009 15:35:21 +0100] rev 662
deleted make_inst3
2009-12-09 tuned
Christian Urban <urbanc@in.tum.de> [Wed, 09 Dec 2009 15:29:36 +0100] rev 661
tuned
2009-12-09 tuned
Christian Urban <urbanc@in.tum.de> [Wed, 09 Dec 2009 15:28:01 +0100] rev 660
tuned
2009-12-09 moved function and tuned comment
Christian Urban <urbanc@in.tum.de> [Wed, 09 Dec 2009 15:24:11 +0100] rev 659
moved function and tuned comment
2009-12-09 improved fun_map_conv
Christian Urban <urbanc@in.tum.de> [Wed, 09 Dec 2009 15:11:49 +0100] rev 658
improved fun_map_conv
2009-12-09 Arbitrary number of fun_map_tacs.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 09 Dec 2009 06:21:09 +0100] rev 657
Arbitrary number of fun_map_tacs.
2009-12-09 Temporarily repeated fun_map_tac 4 times. Cleaning for all examples work.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 09 Dec 2009 05:59:49 +0100] rev 656
Temporarily repeated fun_map_tac 4 times. Cleaning for all examples work.
2009-12-08 tuned code
Christian Urban <urbanc@in.tum.de> [Wed, 09 Dec 2009 00:54:46 +0100] rev 655
tuned code
2009-12-08 tuned the examples and flagged the problematic cleaning lemmas in FSet
Christian Urban <urbanc@in.tum.de> [Wed, 09 Dec 2009 00:03:18 +0100] rev 654
tuned the examples and flagged the problematic cleaning lemmas in FSet
2009-12-08 merged
Christian Urban <urbanc@in.tum.de> [Tue, 08 Dec 2009 23:32:54 +0100] rev 653
merged
2009-12-08 implemented cleaning strategy with fun_map.simps on non-bounded variables; still a few rough edges
Christian Urban <urbanc@in.tum.de> [Tue, 08 Dec 2009 23:30:47 +0100] rev 652
implemented cleaning strategy with fun_map.simps on non-bounded variables; still a few rough edges
2009-12-08 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 08 Dec 2009 23:04:40 +0100] rev 651
merge
2009-12-08 manually cleaned the hard lemma.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 08 Dec 2009 23:04:25 +0100] rev 650
manually cleaned the hard lemma.
2009-12-08 merged
Christian Urban <urbanc@in.tum.de> [Tue, 08 Dec 2009 22:26:01 +0100] rev 649
merged
2009-12-08 decoupled QuotProd from QuotMain and also started new cleaning strategy
Christian Urban <urbanc@in.tum.de> [Tue, 08 Dec 2009 22:24:24 +0100] rev 648
decoupled QuotProd from QuotMain and also started new cleaning strategy
2009-12-08 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 08 Dec 2009 22:05:01 +0100] rev 647
merge
2009-12-08 An example which is hard to lift because of the interplay between lambda_prs and unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 08 Dec 2009 22:03:34 +0100] rev 646
An example which is hard to lift because of the interplay between lambda_prs and unfolding.
2009-12-08 proper formulation of all preservation theorems
Christian Urban <urbanc@in.tum.de> [Tue, 08 Dec 2009 22:02:14 +0100] rev 645
proper formulation of all preservation theorems
2009-12-08 started to reformulate preserve lemmas
Christian Urban <urbanc@in.tum.de> [Tue, 08 Dec 2009 20:55:55 +0100] rev 644
started to reformulate preserve lemmas
2009-12-08 properly set up the prs_rules
Christian Urban <urbanc@in.tum.de> [Tue, 08 Dec 2009 20:34:00 +0100] rev 643
properly set up the prs_rules
2009-12-08 merged
Christian Urban <urbanc@in.tum.de> [Tue, 08 Dec 2009 17:43:32 +0100] rev 642
merged
2009-12-08 added preserve rules to the cleaning_tac
Christian Urban <urbanc@in.tum.de> [Tue, 08 Dec 2009 17:40:58 +0100] rev 641
added preserve rules to the cleaning_tac
2009-12-08 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 08 Dec 2009 17:39:34 +0100] rev 640
merge
2009-12-08 cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 08 Dec 2009 17:35:04 +0100] rev 639
cleaning.
2009-12-08 merged
Christian Urban <urbanc@in.tum.de> [Tue, 08 Dec 2009 17:34:10 +0100] rev 638
merged
2009-12-08 chnaged syntax to "lifting theorem"
Christian Urban <urbanc@in.tum.de> [Tue, 08 Dec 2009 17:33:51 +0100] rev 637
chnaged syntax to "lifting theorem"
2009-12-08 changed names of attributes
Christian Urban <urbanc@in.tum.de> [Tue, 08 Dec 2009 17:30:00 +0100] rev 636
changed names of attributes
2009-12-08 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 08 Dec 2009 16:56:51 +0100] rev 635
merge
2009-12-08 Manual regularization of a goal in FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 08 Dec 2009 16:56:37 +0100] rev 634
Manual regularization of a goal in FSet.
2009-12-08 merged
Christian Urban <urbanc@in.tum.de> [Tue, 08 Dec 2009 16:36:01 +0100] rev 633
merged
2009-12-08 added methods for the lifting_tac and the other tacs
Christian Urban <urbanc@in.tum.de> [Tue, 08 Dec 2009 16:35:40 +0100] rev 632
added methods for the lifting_tac and the other tacs
2009-12-08 make_inst3
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 08 Dec 2009 15:42:29 +0100] rev 631
make_inst3
2009-12-08 Merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 08 Dec 2009 15:12:55 +0100] rev 630
Merge
2009-12-08 trans2 replaced with equals_rsp_tac
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 08 Dec 2009 15:12:36 +0100] rev 629
trans2 replaced with equals_rsp_tac
2009-12-08 corrected name of FSet in ROOT.ML
Christian Urban <urbanc@in.tum.de> [Tue, 08 Dec 2009 14:00:48 +0100] rev 628
corrected name of FSet in ROOT.ML
2009-12-08 Made fset work again to test all.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 08 Dec 2009 13:09:21 +0100] rev 627
Made fset work again to test all.
2009-12-08 Finished the proof of ttt2 and found bug in regularize when trying ttt3.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 08 Dec 2009 13:08:56 +0100] rev 626
Finished the proof of ttt2 and found bug in regularize when trying ttt3.
2009-12-08 Another lambda example theorem proved. Seems it starts working properly.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 08 Dec 2009 13:01:23 +0100] rev 625
Another lambda example theorem proved. Seems it starts working properly.
2009-12-08 Removed pattern from quot_rel_rsp, since list_rel and all used introduced ones cannot be patterned
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 08 Dec 2009 13:00:36 +0100] rev 624
Removed pattern from quot_rel_rsp, since list_rel and all used introduced ones cannot be patterned
2009-12-08 Proper checked map_rsp.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 08 Dec 2009 12:59:38 +0100] rev 623
Proper checked map_rsp.
2009-12-08 Nitpick found a counterexample for one lemma.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 08 Dec 2009 12:36:28 +0100] rev 622
Nitpick found a counterexample for one lemma.
2009-12-08 Added a 'rep_abs' in inj_repabs_trm of babs; and proved two lam examples.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 08 Dec 2009 11:59:16 +0100] rev 621
Added a 'rep_abs' in inj_repabs_trm of babs; and proved two lam examples.
2009-12-08 It also regularizes.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 08 Dec 2009 11:38:58 +0100] rev 620
It also regularizes.
(0) -240 +240 +1000 tip