| Tue, 21 Dec 2010 08:43:39 -0800 | huffman | declare more simp rules, rewrite proofs in Isar-style | changeset | files |
| Tue, 21 Dec 2010 16:41:31 +0100 | hoelzl | merged | changeset | files |
| Tue, 21 Dec 2010 15:00:59 +0100 | hoelzl | use DERIV_intros | changeset | files |
| Tue, 21 Dec 2010 14:50:53 +0100 | hoelzl | generalized monoseq, decseq and incseq; simplified proof for seq_monosub | changeset | files |
| Tue, 21 Dec 2010 15:16:27 +0100 | haftmann | merged | changeset | files |
| Tue, 21 Dec 2010 15:15:55 +0100 | haftmann | proper static closures | changeset | files |
| Tue, 21 Dec 2010 15:15:55 +0100 | haftmann | tuned names | changeset | files |
| Tue, 21 Dec 2010 14:54:23 +0100 | haftmann | renamed mk_id to the more canonical id_const | changeset | files |
| Tue, 21 Dec 2010 14:18:45 +0100 | blanchet | merged | changeset | files |
| Tue, 21 Dec 2010 13:57:35 +0100 | blanchet | better parsing of options, in case the value has '=' | changeset | files |
| Tue, 21 Dec 2010 13:57:19 +0100 | blanchet | show the relation | changeset | files |
| Tue, 21 Dec 2010 10:25:17 +0100 | blanchet | merged | changeset | files |
| Tue, 21 Dec 2010 10:24:56 +0100 | blanchet | renamed "sledgehammer_tactic.ML" to "sledgehammer_tactics.ML" (cf. module name); | changeset | files |
| Tue, 21 Dec 2010 10:18:56 +0100 | blanchet | added "sledgehammer_tac" as possible reconstructor in Mirabelle | changeset | files |
| Tue, 21 Dec 2010 12:48:47 +0100 | wenzelm | merged | changeset | files |