Quot/QuotMain.thy
Fri, 11 Dec 2009 17:03:34 +0100 Christian Urban deleted struct_match by Pattern.match (fixes a problem in LarryInt)
Fri, 11 Dec 2009 15:58:15 +0100 Christian Urban added Int example from Larry
Fri, 11 Dec 2009 08:28:41 +0100 Christian Urban changed error message
Fri, 11 Dec 2009 06:58:31 +0100 Christian Urban reformulated the lemma lifting_procedure as ML value; gave better warning message for injection case
less more (0) -30 -10 -4 tip