- changed back ROOTS
- IsaDof_Manual Monitor should be report.
This commit is contained in:
parent
a69eceb3b4
commit
eda8535b1c
15
Isa_DOF.thy
15
Isa_DOF.thy
|
@ -1549,8 +1549,21 @@ val _ =
|
|||
end (* struct *)
|
||||
\<close>
|
||||
|
||||
ML\<open>
|
||||
text\<open> @{term "a + b"}\<close>
|
||||
|
||||
text\<open>copied from @{file "$ISABELLE_HOME/src/Pure/Thy/thy_output.ML"} \<close>
|
||||
ML\<open> (* copy from *)
|
||||
fun basic_entities name scan pretty =
|
||||
Thy_Output.antiquotation name scan (fn {source, context = ctxt, ...} =>
|
||||
Thy_Output.output ctxt o Thy_Output.maybe_pretty_source pretty ctxt source);
|
||||
|
||||
fun basic_entity name scan = basic_entities name (scan >> single);
|
||||
|
||||
Thy_Output.pretty_term;
|
||||
|
||||
(*
|
||||
basic_entity @{binding term} (Term_Style.parse -- Args.term) pretty_term_style
|
||||
*)
|
||||
\<close>
|
||||
|
||||
section\<open> Testing and Validation \<close>
|
||||
|
|
3
ROOTS
3
ROOTS
|
@ -1,2 +1,3 @@
|
|||
AFP-contribs
|
||||
AFP-contribs/Regular-Sets
|
||||
AFP-contribs/Functional-Automata
|
||||
examples
|
||||
|
|
|
@ -85,7 +85,7 @@ text*[c1::C, x = "''beta''"] \<open> ... suspendisse non arcu malesuada mollis,
|
|||
|
||||
text*[d1::E, a1 = "X3"] \<open> ... phasellus amet id massa nunc, pede suscipit repellendus, ... \<close>
|
||||
|
||||
text*[c2::C, x = "''delta''"] \<open> ... in ut tortor eleifend augue pretium consectetuer... \<close>
|
||||
text*[c2:: C, x = "''delta''"] \<open> ... in ut tortor eleifend augue pretium consectetuer... \<close>
|
||||
|
||||
section*[f::E] \<open> Lectus accumsan velit ultrices, ... }\<close>
|
||||
|
||||
|
|
|
@ -3,7 +3,7 @@ theory "00_Frontmatter"
|
|||
imports "../../../ontologies/technical_report"
|
||||
begin
|
||||
|
||||
open_monitor*[this::article]
|
||||
open_monitor*[this::report]
|
||||
|
||||
(*>*)
|
||||
|
||||
|
|
Loading…
Reference in New Issue