2012-02-16 same as in function_common
Christian Urban <urbanc@in.tum.de> [Thu, 16 Feb 2012 07:14:28 +0000] rev 3120
same as in function_common
2012-02-09 qpaper-jv: merge and add to TODOs in the paper and in front.
Cezary Kaliszyk <cezarykaliszyk@gmail.com> [Thu, 09 Feb 2012 15:18:10 +0100] rev 3119
qpaper-jv: merge and add to TODOs in the paper and in front.
2012-02-09 minor
Cezary Kaliszyk <cezarykaliszyk@gmail.com> [Thu, 09 Feb 2012 14:47:24 +0100] rev 3118
minor
2012-02-03 merged
Christian Urban <urbanc@in.tum.de> [Fri, 03 Feb 2012 15:51:55 +0000] rev 3117
merged
2012-02-03 added FROOT
Christian Urban <urbanc@in.tum.de> [Fri, 03 Feb 2012 15:47:47 +0000] rev 3116
added FROOT
2012-02-03 Use the theorem by Brian, requires new Isabelle.
Cezary Kaliszyk <cezarykaliszyk@gmail.com> [Fri, 03 Feb 2012 16:36:18 +0100] rev 3115
Use the theorem by Brian, requires new Isabelle.
2012-01-31 2 typos found by John Wickerson in QPaper
Christian Urban <urbanc@in.tum.de> [Tue, 31 Jan 2012 16:26:36 +0000] rev 3114
2 typos found by John Wickerson in QPaper
2012-01-24 repaired all slides
Christian Urban <urbanc@in.tum.de> [Tue, 24 Jan 2012 17:43:07 +0000] rev 3113
repaired all slides
2012-01-24 tuned make-file
Christian Urban <urbanc@in.tum.de> [Tue, 24 Jan 2012 16:51:01 +0000] rev 3112
tuned make-file
2012-01-24 made all papers work again
Christian Urban <urbanc@in.tum.de> [Tue, 24 Jan 2012 14:29:07 +0000] rev 3111
made all papers work again
2012-01-24 added a session entry in order to quickly build the heap file (tests took too long)
Christian Urban <urbanc@in.tum.de> [Tue, 24 Jan 2012 14:05:24 +0000] rev 3110
added a session entry in order to quickly build the heap file (tests took too long)
2012-01-16 commented out parts of TypeScheme1 in order to run all tests
Christian Urban <urbanc@in.tum.de> [Mon, 16 Jan 2012 13:53:35 +0000] rev 3109
commented out parts of TypeScheme1 in order to run all tests
2012-01-16 updated to Isabelle 16 January
Christian Urban <urbanc@in.tum.de> [Mon, 16 Jan 2012 12:42:47 +0000] rev 3108
updated to Isabelle 16 January
2012-01-09 merged
Christian Urban <urbanc@in.tum.de> [Mon, 09 Jan 2012 10:45:12 +0000] rev 3107
merged
2012-01-09 added the simple fixes for the paper
Christian Urban <urbanc@in.tum.de> [Mon, 09 Jan 2012 10:12:46 +0000] rev 3106
added the simple fixes for the paper
2012-01-04 added an FCB for res (will not define evry function, but is a good datapoint)
Christian Urban <urbanc@in.tum.de> [Wed, 04 Jan 2012 17:42:16 +0000] rev 3105
added an FCB for res (will not define evry function, but is a good datapoint)
2012-01-03 updated to explicit set type constructor (post Isabelle 3rd January)
Christian Urban <urbanc@in.tum.de> [Tue, 03 Jan 2012 11:43:27 +0000] rev 3104
updated to explicit set type constructor (post Isabelle 3rd January)
2012-01-03 proved that generalisation is closed under substitution
Christian Urban <urbanc@in.tum.de> [Tue, 03 Jan 2012 01:42:10 +0000] rev 3103
proved that generalisation is closed under substitution
2012-01-02 added definition for generalisation of type schemes (for paper)
Christian Urban <urbanc@in.tum.de> [Mon, 02 Jan 2012 16:13:16 +0000] rev 3102
added definition for generalisation of type schemes (for paper)
2011-12-29 added two eqvt lemmas for fset-operators
Christian Urban <urbanc@in.tum.de> [Thu, 29 Dec 2011 18:05:13 +0000] rev 3101
added two eqvt lemmas for fset-operators
2011-12-29 separated the two versions of type schemes into two files
Christian Urban <urbanc@in.tum.de> [Thu, 29 Dec 2011 15:56:54 +0000] rev 3100
separated the two versions of type schemes into two files
2011-12-29 added notes by referees to comment about our changes
Christian Urban <urbanc@in.tum.de> [Thu, 29 Dec 2011 12:40:36 +0000] rev 3099
added notes by referees to comment about our changes
2011-12-29 made the paper running again
Christian Urban <urbanc@in.tum.de> [Thu, 29 Dec 2011 12:37:38 +0000] rev 3098
made the paper running again
2011-12-23 included Pi theory in tests
Christian Urban <urbanc@in.tum.de> [Fri, 23 Dec 2011 15:04:01 +0000] rev 3097
included Pi theory in tests
2011-12-23 added file by Kirstin
Christian Urban <urbanc@in.tum.de> [Fri, 23 Dec 2011 10:36:34 +0000] rev 3096
added file by Kirstin
2011-12-22 merged
Christian Urban <urbanc@in.tum.de> [Thu, 22 Dec 2011 13:10:58 +0000] rev 3095
merged
2011-12-22 moved TODO into the paper
Christian Urban <urbanc@in.tum.de> [Thu, 22 Dec 2011 05:15:37 +0000] rev 3094
moved TODO into the paper
2011-12-22 merged
Christian Urban <urbanc@in.tum.de> [Thu, 22 Dec 2011 04:47:05 +0000] rev 3093
merged
2011-12-22 some slight tuning
Christian Urban <urbanc@in.tum.de> [Thu, 22 Dec 2011 04:46:37 +0000] rev 3092
some slight tuning
2011-12-22 the default sort for type-variables in nominal specifications is fs; it is automatically addded
Christian Urban <urbanc@in.tum.de> [Thu, 22 Dec 2011 13:10:30 +0000] rev 3091
the default sort for type-variables in nominal specifications is fs; it is automatically addded
2011-12-22 fixed problem with equivariance for beta_star
Christian Urban <urbanc@in.tum.de> [Thu, 22 Dec 2011 04:35:01 +0000] rev 3090
fixed problem with equivariance for beta_star
2011-12-21 Reorder constructors to match Lambda
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 21 Dec 2011 17:05:00 +0900] rev 3089
Reorder constructors to match Lambda
2011-12-21 SFT/LambdaTerms: rename 'var' to 'name' to match Lambda.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 21 Dec 2011 15:47:42 +0900] rev 3088
SFT/LambdaTerms: rename 'var' to 'name' to match Lambda.
2011-12-21 SFT: Rename Lambda to LambdaTerms, rename constants to match Lambda, remove smt proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 21 Dec 2011 15:43:58 +0900] rev 3087
SFT: Rename Lambda to LambdaTerms, rename constants to match Lambda, remove smt proofs.
2011-12-21 Remove transitivity from the definition of One_star and show it instead.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 21 Dec 2011 14:25:05 +0900] rev 3086
Remove transitivity from the definition of One_star and show it instead.
2011-12-21 Port CR_Takahashi from Nominal1, no more "sorry" in BetaCR.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 21 Dec 2011 13:06:09 +0900] rev 3085
Port CR_Takahashi from Nominal1, no more "sorry" in BetaCR.
2011-12-20 Add Sigma.thy, an example that defines a sigma-calculus in the style of Peter Homeier's HOL4 formalization.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 20 Dec 2011 18:07:48 +0900] rev 3084
Add Sigma.thy, an example that defines a sigma-calculus in the style of Peter Homeier's HOL4 formalization.
2011-12-20 Update Quotient FIXME-TODO, some issues were already fixed.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 20 Dec 2011 17:58:34 +0900] rev 3083
Update Quotient FIXME-TODO, some issues were already fixed.
2011-12-20 Added an initial version of qpaper-jv and a TODO of things to write about.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 20 Dec 2011 17:54:53 +0900] rev 3082
Added an initial version of qpaper-jv and a TODO of things to write about.
2011-12-20 Remove 'HERE1' and 'HERE3'.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 20 Dec 2011 16:49:03 +0900] rev 3081
Remove 'HERE1' and 'HERE3'.
2011-12-20 Lift substitution of an Abstraction for BetaCR :)
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 20 Dec 2011 16:12:32 +0900] rev 3080
Lift substitution of an Abstraction for BetaCR :)
2011-12-20 Tuned renaming
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 20 Dec 2011 11:40:04 +0900] rev 3079
Tuned renaming
2011-12-19 Retry Beta using a reduction relation and its reflexive-symmetric-transitive closure.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Dec 2011 16:39:20 +0900] rev 3078
Retry Beta using a reduction relation and its reflexive-symmetric-transitive closure.
2011-12-19 Disproved the property described as 'Tzevelakos'.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Dec 2011 14:20:25 +0900] rev 3077
Disproved the property described as 'Tzevelakos'.
2011-12-18 partially localised the parsing process using functions fron Datatype
Christian Urban <urbanc@in.tum.de> [Sun, 18 Dec 2011 00:42:32 +0000] rev 3076
partially localised the parsing process using functions fron Datatype
2011-12-17 updated
Christian Urban <urbanc@in.tum.de> [Sat, 17 Dec 2011 20:03:37 +0000] rev 3075
updated
2011-12-17 updated in stable branch Nominal2-Isabelle2011-1
Christian Urban <urbanc@in.tum.de> [Sat, 17 Dec 2011 17:51:01 +0000] rev 3074
updated in stable branch
2011-12-17 updated all examples in stable branch Nominal2-Isabelle2011-1
Christian Urban <urbanc@in.tum.de> [Sat, 17 Dec 2011 17:31:40 +0000] rev 3073
updated all examples in stable branch
2011-12-17 deleted Manual directory in stable branch Nominal2-Isabelle2011-1
Christian Urban <urbanc@in.tum.de> [Sat, 17 Dec 2011 17:10:11 +0000] rev 3072
deleted Manual directory in stable branch
2011-12-17 cleaned examples for stable branch Nominal2-Isabelle2011-1
Christian Urban <urbanc@in.tum.de> [Sat, 17 Dec 2011 17:08:47 +0000] rev 3071
cleaned examples for stable branch
2011-12-17 cleaned all papers from the stable branch Nominal2-Isabelle2011-1
Christian Urban <urbanc@in.tum.de> [Sat, 17 Dec 2011 17:03:01 +0000] rev 3070
cleaned all papers from the stable branch
2011-12-17 cleaned Attic in stable branch Nominal2-Isabelle2011-1
Christian Urban <urbanc@in.tum.de> [Sat, 17 Dec 2011 16:58:11 +0000] rev 3069
cleaned Attic in stable branch
2011-12-17 backported no_eqvt changeset 1afcbaf4242b Nominal2-Isabelle2011-1
Christian Urban <urbanc@in.tum.de> [Sat, 17 Dec 2011 16:57:25 +0000] rev 3068
backported no_eqvt changeset 1afcbaf4242b
2011-12-17 Started Nominal2-Isabelle2011-1 branch and backported changeset 32abaea424bd Nominal2-Isabelle2011-1
Christian Urban <urbanc@in.tum.de> [Sat, 17 Dec 2011 16:36:51 +0000] rev 3067
Started Nominal2-Isabelle2011-1 branch and backported changeset 32abaea424bd
2011-12-16 Beta: equ and equ2 are not the same relations, equ2 seems not to be beta-eta equality.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 16 Dec 2011 16:01:12 +0900] rev 3066
Beta: equ and equ2 are not the same relations, equ2 seems not to be beta-eta equality.
2011-12-15 updated to lates changes in the datatype package
Christian Urban <urbanc@in.tum.de> [Thu, 15 Dec 2011 16:20:42 +0000] rev 3065
updated to lates changes in the datatype package
2011-12-15 a bit more on alpha-beta-equated terms
Christian Urban <urbanc@in.tum.de> [Thu, 15 Dec 2011 16:20:11 +0000] rev 3064
a bit more on alpha-beta-equated terms
2011-12-14 generated the correct thm-list for showing that qfv are equal to support
Christian Urban <urbanc@in.tum.de> [Wed, 14 Dec 2011 01:32:42 +0000] rev 3063
generated the correct thm-list for showing that qfv are equal to support
2011-12-13 updated to Isabelle 13 Dec
Christian Urban <urbanc@in.tum.de> [Tue, 13 Dec 2011 09:39:56 +0000] rev 3062
updated to Isabelle 13 Dec
2011-12-06 updated to Isabelle 6 Dec (thanks to Odrej Kuncar)
Christian Urban <urbanc@in.tum.de> [Tue, 06 Dec 2011 23:42:19 +0000] rev 3061
updated to Isabelle 6 Dec (thanks to Odrej Kuncar)
(0) -3000 -1000 -300 -100 -60 +60 +100 tip