trivial
authorChristian Urban <urbanc@in.tum.de>
Sat, 12 Dec 2009 13:53:46 +0100
changeset 731 e16523f01908
parent 730 66f44de8bf5b
child 732 33cd648df179
trivial
Quot/Examples/LFex.thy
--- 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