| Fri, 24 May 2013 16:43:37 +0200 | blanchet | improved handling of free variables' types in Isar proofs | changeset | files |
| Fri, 24 May 2013 11:08:25 +0200 | blanchet | pass noninteractive flag -- necessary to run under CASC's "runsolver" program | changeset | files |
| Fri, 24 May 2013 11:08:22 +0200 | blanchet | untabify | changeset | files |
| Thu, 23 May 2013 14:22:49 +0200 | noschinl | more lemmas for sorted_list_of_set | changeset | files |
| Thu, 23 May 2013 13:51:21 +1000 | kleing | prefer object equality | changeset | files |
| Thu, 23 May 2013 11:39:40 +1000 | kleing | slightly clearer formulation | changeset | files |
| Wed, 22 May 2013 22:56:17 +0200 | haftmann | interpretation must always operate on the last element in a local theory stack, not on all elements: interpretated facts must disappear after pop from local theory stack, and transfer from last target is not enough | changeset | files |