author | Christian Urban <urbanc@in.tum.de> |
Sat, 12 Dec 2009 13:53:46 +0100 | |
changeset 731 | e16523f01908 |
parent 730 | 66f44de8bf5b |
child 732 | 33cd648df179 |
--- a/Quot/Examples/LFex.thy Sat Dec 12 02:01:33 2009 +0100 +++ b/Quot/Examples/LFex.thy Sat Dec 12 13:53:46 2009 +0100 @@ -259,7 +259,7 @@ ML_prf {* PolyML.profiling 1 *} ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *} *) -done + done (* Does not work: lemma