| Mon, 17 May 2010 15:21:11 +0200 | blanchet | make sure chained facts don't pop up in the metis proof | changeset | files |
| Mon, 17 May 2010 12:15:37 +0200 | blanchet | fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably | changeset | files |
| Mon, 17 May 2010 10:18:14 +0200 | blanchet | generate proper arity declarations for TFrees for SPASS's DFG format; | changeset | files |
| Mon, 17 May 2010 10:16:54 +0200 | blanchet | identify common SPASS error more clearly | changeset | files |
| Mon, 17 May 2010 08:40:17 -0700 | huffman | remove simp attribute from power2_eq_1_iff | changeset | files |
| Mon, 17 May 2010 10:58:58 +0200 | haftmann | dropped old Library/Word.thy and toy example ex/Adder.thy | changeset | files |
| Mon, 17 May 2010 10:58:31 +0200 | haftmann | dropped old Library/Word.thy and toy example ex/Adder.thy | changeset | files |
| Tue, 18 May 2010 00:01:03 +0200 | wenzelm | do not open Legacy by default; | changeset | files |