Enclosed end_theory in text antiquotation to make LaTeX happy.
authorberghofe
Wed Sep 19 12:17:13 2007 +0200 (2007-09-19)
changeset 2464466ef82187de1
parent 24643 d5e4b170d132
child 24645 1af302128da2
Enclosed end_theory in text antiquotation to make LaTeX happy.
src/HOL/Main.thy
     1.1 --- a/src/HOL/Main.thy	Wed Sep 19 11:50:07 2007 +0200
     1.2 +++ b/src/HOL/Main.thy	Wed Sep 19 12:17:13 2007 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4  
     1.5    \medskip Late clause setup: installs \emph{all} known theorems
     1.6    into the clause cache; cf.\ theory @{text ATP_Linkup}. 
     1.7 -  FIXME: delete once end_theory actions are installed!
     1.8 +  FIXME: delete once @{text end_theory} actions are installed!
     1.9  *}
    1.10  
    1.11  setup ResAxioms.clause_cache_setup