Quot/Examples/LFex.thy
changeset 731 e16523f01908
parent 705 f51c6069cd17
child 766 df053507edba
--- 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