equal
deleted
inserted
replaced
1353 |
1353 |
1354 \railalias{thmdeps}{thm\_deps} |
1354 \railalias{thmdeps}{thm\_deps} |
1355 \railterm{thmdeps} |
1355 \railterm{thmdeps} |
1356 |
1356 |
1357 \begin{rail} |
1357 \begin{rail} |
1358 thmscontaining (term * ) |
1358 thmscontaining ('(' nat ')')? (term * ) |
1359 ; |
1359 ; |
1360 thmdeps thmrefs |
1360 thmdeps thmrefs |
1361 ; |
1361 ; |
1362 \end{rail} |
1362 \end{rail} |
1363 |
1363 |
1389 packages, such as $\isarkeyword{datatype}$. |
1389 packages, such as $\isarkeyword{datatype}$. |
1390 |
1390 |
1391 \item [$\isarkeyword{thms_containing}~\vec t$] retrieves facts from the theory |
1391 \item [$\isarkeyword{thms_containing}~\vec t$] retrieves facts from the theory |
1392 or proof context containing all of the constants or variables occurring in |
1392 or proof context containing all of the constants or variables occurring in |
1393 terms $\vec t$. Note that giving the empty list yields \emph{all} currently |
1393 terms $\vec t$. Note that giving the empty list yields \emph{all} currently |
1394 known facts. |
1394 known facts. An optional limit for the number printed facts may be given; |
|
1395 the default is 40. |
1395 |
1396 |
1396 \item [$\isarkeyword{thm_deps}~\vec a$] visualizes dependencies of facts, |
1397 \item [$\isarkeyword{thm_deps}~\vec a$] visualizes dependencies of facts, |
1397 using Isabelle's graph browser tool (see also \cite{isabelle-sys}). |
1398 using Isabelle's graph browser tool (see also \cite{isabelle-sys}). |
1398 |
1399 |
1399 \item [$\isarkeyword{print_facts}$] prints any named facts of the current |
1400 \item [$\isarkeyword{print_facts}$] prints any named facts of the current |