Thu, 11 Feb 2010 08:44:19 +0100 | nipkow | inductive vs inductive_set explanation | changeset | files |
Thu, 11 Feb 2010 00:45:02 +0100 | wenzelm | modernized translations; | changeset | files |
Wed, 10 Feb 2010 23:53:46 +0100 | wenzelm | modernized translations; | changeset | files |
Wed, 10 Feb 2010 19:37:34 +0100 | wenzelm | renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL; | changeset | files |
Wed, 10 Feb 2010 17:05:40 +0100 | berghofe | merged | changeset | files |
Wed, 10 Feb 2010 17:05:18 +0100 | berghofe | Fixed bug in code for guessing the name of the variable representing the freshness context. | changeset | files |
Wed, 10 Feb 2010 15:52:12 +0100 | haftmann | dropped last occurence of the linlinordered accident | changeset | files |