Fri, 16 Mar 2007 17:17:36 +0100 | urbanc | adjusted for the example file SOS.thy | changeset | files |
Fri, 16 Mar 2007 17:12:52 +0100 | urbanc | added formalisations of typical SOS-proofs | changeset | files |
Fri, 16 Mar 2007 17:09:18 +0100 | urbanc | added eqvt-lemmas for integers and eqvt-tagged the lemma append_eqvt | changeset | files |
Fri, 16 Mar 2007 16:40:49 +0100 | dixon | removed safe elim flag of trueElim and notFalseElim for testing. | changeset | files |
Fri, 16 Mar 2007 16:37:52 +0100 | dixon | added safe intro rules for removing "True" subgoals as well as "~ False" ones. | changeset | files |
Wed, 14 Mar 2007 21:52:26 +0100 | huffman | move sqrt_divide_self_eq to NthRoot.thy | changeset | files |