From 0f9b6731af02315e50fa1f8ada19ba1df1e33cda Mon Sep 17 00:00:00 2001 From: bu Date: Fri, 12 Jun 2020 15:00:49 +0200 Subject: [PATCH 1/4] replaced structure with legecy code: Pure_Syn_Ext. --- src/DOF/Isa_DOF.thy | 60 ++++++++++++++++++++++++++------------------- 1 file changed, 35 insertions(+), 25 deletions(-) diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index f76d8ce..b902255 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -942,28 +942,8 @@ fun document_command markdown (loc, txt) = *) -ML\ Pure_Syn.document_command; -structure Pure_Syn_Ext = -struct -(* This interface function has not been exported from Pure_Syn (2018); - it should replace - Thy_Output.output_text: Toplevel.state -> {markdown: bool} -> Input.source -> string (2017) *) -fun output_document state markdown src = - let - val ctxt = Toplevel.presentation_context state; - val _ = Context_Position.report ctxt - (Input.pos_of src) - (Markup.language_document (Input.is_delimited src)); - in Thy_Output.output_document ctxt markdown src end; - (* this thing converts also source to (latex) string ... *) - -end; - -Pure_Syn_Ext.output_document : Toplevel.state -> {markdown: bool} -> Input.source -> Latex.text list; - -\ ML\ structure ODL_Command_Parser = @@ -1213,6 +1193,31 @@ fun update_instance_command (((oid:string,pos),cid_pos), end +(* +fun gen_enriched_document_command cid_transform attr_transform + markdown + (((((oid,pos),cid_pos), doc_attrs) : meta_args_t, + xstring_opt:(xstring * Position.T) option), + toks:Input.source) + : theory -> theory = + let val toplvl = Toplevel.theory_toplevel + + fun check thy = let val ctxt = Toplevel.presentation_context (toplvl thy); + val _ = Context_Position.report ctxt + (Input.pos_of toks) + (Markup.language_document (Input.is_delimited toks)); + in thy end + + (* as side-effect, generates markup *) + fun check_n_tex_text thy = (Pure_Syn_Ext.output_document(toplvl thy) markdown toks, thy) + + (* ... generating the level-attribute syntax *) + in + ( create_and_check_docitem false oid pos (cid_transform cid_pos) (attr_transform doc_attrs) + #> (* (snd o check_n_tex_text) *) check ) + (* Thanks Frederic Tuong! ! ! *) + end; +*) fun gen_enriched_document_command cid_transform attr_transform markdown @@ -1220,17 +1225,22 @@ fun gen_enriched_document_command cid_transform attr_transform xstring_opt:(xstring * Position.T) option), toks:Input.source) : theory -> theory = - let - (* as side-effect, generates markup *) - fun check_text thy = (Pure_Syn_Ext.output_document(Toplevel.theory_toplevel thy) markdown toks; - thy) + let val toplvl = Toplevel.theory_toplevel + (* checking and markup generation *) + fun check thy = let val ctxt = Toplevel.presentation_context (toplvl thy); + val _ = Context_Position.report ctxt + (Input.pos_of toks) + (Markup.language_document (Input.is_delimited toks)); + in thy end + (* ... generating the level-attribute syntax *) in ( create_and_check_docitem false oid pos (cid_transform cid_pos) (attr_transform doc_attrs) - #> check_text) + #> check ) (* Thanks Frederic Tuong! ! ! *) end; + (* General criticism : attributes like "level" were treated here in the kernel instead of dragging them out into the COL -- bu *) From d86c713e37e56aab25b89f9aff06ac9af35cb821 Mon Sep 17 00:00:00 2001 From: bu Date: Fri, 12 Jun 2020 16:36:54 +0200 Subject: [PATCH 2/4] first running study of OoO - Presentation --- src/tests/OutOfOrderPresntn.thy | 94 +++++++++++++++++++++++++++++++++ 1 file changed, 94 insertions(+) create mode 100644 src/tests/OutOfOrderPresntn.thy diff --git a/src/tests/OutOfOrderPresntn.thy b/src/tests/OutOfOrderPresntn.thy new file mode 100644 index 0000000..0145868 --- /dev/null +++ b/src/tests/OutOfOrderPresntn.thy @@ -0,0 +1,94 @@ +(************************************************************************* + * Copyright (C) + * 2019 The University of Exeter + * 2018-2019 The University of Paris-Saclay + * 2018 The University of Sheffield + * + * License: + * This program can be redistributed and/or modified under the terms + * of the 2-clause BSD-style license. + * + * SPDX-License-Identifier: BSD-2-Clause + *************************************************************************) + +theory + OutOfOrderPresntn +imports + "Isabelle_DOF.Conceptual" +keywords "text-" :: document_body +begin + +section\Elementary Creation of Doc-items and Access of their Attibutes\ + + +text\Current status:\ +print_doc_classes +print_doc_items + +(* this corresponds to low-level accesses : *) +ML\ +val {docobj_tab={tab = docitem_tab, ...},docclass_tab, ISA_transformer_tab, monitor_tab,...} + = DOF_core.get_data @{context}; +Symtab.dest docitem_tab; +Symtab.dest docclass_tab; +\ + + + +ML\ +Pure_Syn.document_command; + +fun output_document state markdown src = + let + val ctxt = Toplevel.presentation_context state; + val _ = Context_Position.report ctxt + (Input.pos_of src) + (Markup.language_document (Input.is_delimited src)); + in Thy_Output.output_document ctxt markdown src end; + (* this thing converts also source to (latex) text ... *) + +output_document : Toplevel.state -> {markdown: bool} -> Input.source -> Latex.text list; + + +fun gen_enriched_document_command2 cid_transform attr_transform + markdown + (((((oid,pos),cid_pos), doc_attrs) : ODL_Command_Parser.meta_args_t, + xstring_opt:(xstring * Position.T) option), + toks:Input.source) + : theory -> theory = + let val toplvl = Toplevel.theory_toplevel + + (* as side-effect, generates markup *) + fun check_n_tex_text thy = let val text = output_document (toplvl thy) markdown toks + val file = {path = Path.make [oid ^ "_snippet.tex"], + pos = @{here}, + content = Latex.output_text text} + val _ = Generated_Files.write_file (Path.make ["latex_test"]) file + val _ = writeln (Latex.output_text text) + in thy end + + (* ... generating the level-attribute syntax *) + in + ( ODL_Command_Parser.create_and_check_docitem false oid pos (cid_transform cid_pos) (attr_transform doc_attrs) + #> check_n_tex_text ) + end; + +val _ = + Outer_Syntax.command ("text-", @{here}) "formal comment macro" + (ODL_Command_Parser.attributes -- Parse.opt_target -- Parse.document_source + >> (Toplevel.theory o (gen_enriched_document_command2 I I {markdown = true} ))); + +\ + + +text\And here a tex - text macro.\ + +text-[dfgdfg::B]\ Lorem ipsum ... @{thm refl} \ + +(*<*) +text\Final Status:\ +print_doc_items +print_doc_classes + +end +(*>*) From 4717925eea841cd91dfbf2ae107d67cea33e0bc6 Mon Sep 17 00:00:00 2001 From: bu Date: Tue, 16 Jun 2020 09:08:36 +0200 Subject: [PATCH 3/4] Zwischenzustand OoO Generation --- src/DOF/Isa_COL.thy | 8 +-- src/DOF/Isa_DOF.thy | 86 +++++++++++++++------------------ src/tests/OutOfOrderPresntn.thy | 9 +++- 3 files changed, 51 insertions(+), 52 deletions(-) diff --git a/src/DOF/Isa_COL.thy b/src/DOF/Isa_COL.thy index 7a9eacf..c9ca1c9 100644 --- a/src/DOF/Isa_COL.thy +++ b/src/DOF/Isa_COL.thy @@ -80,7 +80,7 @@ fun enriched_document_command level = NONE => doc_attrs | SOME(NONE) => (("level",@{here}),"None")::doc_attrs | SOME(SOME x) => (("level",@{here}),"Some("^ Int.toString x ^"::int)")::doc_attrs - in gen_enriched_document_command I transform end; + in gen_enriched_document_command {inline=true} I transform end; val enriched_document_command_macro = enriched_document_command (* TODO ... *) @@ -92,7 +92,7 @@ fun enriched_formal_statement_command ncid (S: (string * string) list) = | _ => X) fun transform_attr doc_attrs = (map (fn(cat,tag) => ((cat,@{here}),tag)) S) @ (("formal_results",@{here}),"([]::thm list)")::doc_attrs - in gen_enriched_document_command transform_cid transform_attr end; + in gen_enriched_document_command {inline=true} transform_cid transform_attr end; fun assertion_cmd'((((((oid,pos),cid_pos),doc_attrs),name_opt:string option),modes : string list), @@ -104,7 +104,9 @@ fun assertion_cmd'((((((oid,pos),cid_pos),doc_attrs),name_opt:string option),mod fun mks thy = case DOF_core.get_object_global_opt oid thy of SOME NONE => (error("update of declared but not created doc_item:" ^ oid)) | SOME _ => (update_instance_command (((oid,pos),cid_pos),conv_attrs' thy) thy) - | NONE => (create_and_check_docitem false oid pos cid_pos (conv_attrs thy) thy) + | NONE => (create_and_check_docitem + {is_monitor = false} {is_inline = false} + oid pos cid_pos (conv_attrs thy) thy) val check = (assert_cmd name_opt modes prop) o Proof_Context.init_global in (* Toplevel.keep (check o Toplevel.context_of) *) diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index b902255..6ea0717 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -166,8 +166,10 @@ struct type docobj = {pos : Position.T, thy_name : string, - value : term, - id : serial, cid : string} + value : term, + inline : bool, + id : serial, + cid : string} type docobj_tab ={tab : (docobj option) Symtab.table, maxano : int @@ -570,9 +572,10 @@ fun get_value_local oid ctxt = case get_object_local oid ctxt of (* missing : setting terms to ground (no type-schema vars, no schema vars. )*) fun update_value_global oid upd thy = case get_object_global oid thy of - SOME{pos,thy_name,value,id,cid} => + SOME{pos,thy_name,value,inline,id,cid} => let val tab' = Symtab.update(oid,SOME{pos=pos,thy_name=thy_name, - value=upd value,id=id, cid=cid}) + value=upd value,id=id, + inline=inline,cid=cid}) in map_data_global (upd_docobj_tab(fn{tab,maxano}=>{tab=tab' tab,maxano=maxano})) thy end | NONE => error("undefined doc object: "^oid) @@ -623,11 +626,14 @@ fun writeln_docrefs ctxt = let val {tab,...} = #docobj_tab(get_data ctxt) fun print_doc_items b ctxt = let val {docobj_tab={tab = x, ...},...}= get_data ctxt; - val _ = writeln "====================================="; - fun print_item (n, SOME({cid,id,pos,thy_name,value})) = + val _ = writeln "====================================="; + fun dfg true = "true" + |dfg false= "false" + fun print_item (n, SOME({cid,id,pos,thy_name,inline,value})) = (writeln ("docitem: "^n); writeln (" type: "^cid); writeln (" origine: "^thy_name); + writeln (" inline: "^dfg inline); writeln (" value: "^(Syntax.string_of_term ctxt value)) ) | print_item (n, NONE) = @@ -1018,7 +1024,7 @@ fun cid_2_cidType cid_long thy = fun base_default_term thy cid_long = Const(@{const_name "undefined"},cid_2_cidType thy cid_long) -fun check_classref is_monitor (SOME(cid,pos')) thy = +fun check_classref {is_monitor=is_monitor} (SOME(cid,pos')) thy = let val cid_long = DOF_core.read_cid_global thy cid @@ -1129,7 +1135,7 @@ fun register_oid_cid_in_open_monitors oid pos cid_long thy = rejected_cids=rejected_cids, automatas=aS}) tab end fun update_trace mon_oid = DOF_core.update_value_global mon_oid (def_trans mon_oid) - val update_automatons = DOF_core.upd_monitor_tabs(fold update_info delta_autoS) + val update_automatons = DOF_core.upd_monitor_tabs(fold update_info delta_autoS) in thy |> (* update traces of all enabled monitors *) fold (update_trace) (enabled_monitors) |> (* check class invariants of enabled monitors *) @@ -1139,7 +1145,7 @@ fun register_oid_cid_in_open_monitors oid pos cid_long thy = end -fun create_and_check_docitem is_monitor oid pos cid_pos doc_attrs thy = +fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos doc_attrs thy = let val id = serial (); val _ = Position.report pos (docref_markup true oid id pos); (* creates a markup label for this position and reports it to the PIDE framework; @@ -1152,11 +1158,12 @@ fun create_and_check_docitem is_monitor oid pos cid_pos doc_attrs thy = fun conv_attrs ((lhs, pos), rhs) = (markup2string lhs,pos,"=", Syntax.read_term_global thy rhs) val assns' = map conv_attrs doc_attrs val (value_term, _(*ty*), _) = calc_update_term thy cid_long assns' defaults - val check_inv = (DOF_core.get_class_invariant cid_long thy oid {is_monitor=is_monitor}) + val check_inv = (DOF_core.get_class_invariant cid_long thy oid is_monitor) o Context.Theory in thy |> DOF_core.define_object_global (oid, {pos = pos, thy_name = Context.theory_name thy, value = value_term, + inline = is_inline, id = id, cid = cid_long}) |> register_oid_cid_in_open_monitors oid pos cid_long @@ -1175,7 +1182,7 @@ fun update_instance_command (((oid:string,pos),cid_pos), val _ = Context_Position.report ctxt pos markup; in cid end | NONE => error("undefined doc_class.") - val cid_long = check_classref false cid_pos thy + val cid_long = check_classref {is_monitor = false} cid_pos thy val _ = if cid_long = DOF_core.default_cid orelse cid = cid_long then () else error("incompatible classes:"^cid^":"^cid_long) @@ -1193,33 +1200,8 @@ fun update_instance_command (((oid:string,pos),cid_pos), end -(* -fun gen_enriched_document_command cid_transform attr_transform - markdown - (((((oid,pos),cid_pos), doc_attrs) : meta_args_t, - xstring_opt:(xstring * Position.T) option), - toks:Input.source) - : theory -> theory = - let val toplvl = Toplevel.theory_toplevel - fun check thy = let val ctxt = Toplevel.presentation_context (toplvl thy); - val _ = Context_Position.report ctxt - (Input.pos_of toks) - (Markup.language_document (Input.is_delimited toks)); - in thy end - - (* as side-effect, generates markup *) - fun check_n_tex_text thy = (Pure_Syn_Ext.output_document(toplvl thy) markdown toks, thy) - - (* ... generating the level-attribute syntax *) - in - ( create_and_check_docitem false oid pos (cid_transform cid_pos) (attr_transform doc_attrs) - #> (* (snd o check_n_tex_text) *) check ) - (* Thanks Frederic Tuong! ! ! *) - end; -*) - -fun gen_enriched_document_command cid_transform attr_transform +fun gen_enriched_document_command {inline=is_inline} cid_transform attr_transform markdown (((((oid,pos),cid_pos), doc_attrs) : meta_args_t, xstring_opt:(xstring * Position.T) option), @@ -1235,7 +1217,8 @@ fun gen_enriched_document_command cid_transform attr_transform (* ... generating the level-attribute syntax *) in - ( create_and_check_docitem false oid pos (cid_transform cid_pos) (attr_transform doc_attrs) + ( create_and_check_docitem {is_monitor=false} {is_inline=is_inline} + oid pos (cid_transform cid_pos) (attr_transform doc_attrs) #> check ) (* Thanks Frederic Tuong! ! ! *) end; @@ -1246,7 +1229,9 @@ fun gen_enriched_document_command cid_transform attr_transform fun open_monitor_command ((((oid,pos),cid_pos), doc_attrs) : meta_args_t) = let fun o_m_c oid pos cid_pos doc_attrs thy = create_and_check_docitem - true oid pos cid_pos doc_attrs thy + {is_monitor=true} (* this is a monitor *) + {is_inline=false} (* monitors are always inline *) + oid pos cid_pos doc_attrs thy fun compute_enabled_set cid thy = case DOF_core.get_doc_class_global cid thy of SOME X => let val ralph = RegExpInterface.alphabet (#rejectS X) @@ -1311,13 +1296,15 @@ val _ = val _ = Outer_Syntax.command ("text*", @{here}) "formal comment (primary style)" (attributes -- Parse.opt_target -- Parse.document_source - >> (Toplevel.theory o (gen_enriched_document_command I I {markdown = true} ))); + >> (Toplevel.theory o (gen_enriched_document_command {inline=true} + I I {markdown = true} ))); (* This is just a stub at present *) val _ = Outer_Syntax.command ("text-macro*", @{here}) "formal comment macro" (attributes -- Parse.opt_target -- Parse.document_source - >> (Toplevel.theory o (gen_enriched_document_command I I {markdown = true} ))); + >> (Toplevel.theory o (gen_enriched_document_command {inline=false} (* declare as macro *) + I I {markdown = true} ))); val _ = Outer_Syntax.command @{command_keyword "declare_reference*"} @@ -1465,12 +1452,15 @@ struct val basic_entity = Thy_Output.antiquotation_pretty_source : binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory; -fun check_and_mark ctxt cid_decl (str:{strict_checking: bool}) pos name = +fun check_and_mark ctxt cid_decl (str:{strict_checking: bool}) {inline=inline_req} pos name = let val thy = Proof_Context.theory_of ctxt; in if DOF_core.is_defined_oid_global name thy - then let val {pos=pos_decl,id,cid,...} = the(DOF_core.get_object_global name thy) + then let val {pos=pos_decl,id,cid,inline,...} = the(DOF_core.get_object_global name thy) + val _ = if not inline_req + then if inline then () else error("referred text-element is macro! (try option display)") + else if not inline then () else error("referred text-element is no macro!") val markup = docref_markup false name id pos_decl; val _ = Context_Position.report ctxt pos markup; (* this sends a report for a ref application to the PIDE interface ... *) @@ -1486,7 +1476,8 @@ fun check_and_mark ctxt cid_decl (str:{strict_checking: bool}) pos name = else error("undefined document reference: "^name) end -val _ = check_and_mark : Proof.context -> string -> {strict_checking: bool} -> +val _ = check_and_mark : Proof.context -> string -> + {strict_checking: bool} -> {inline:bool} -> Position.T -> Symtab.key -> unit (* generic syntax for doc_class links. *) @@ -1507,8 +1498,9 @@ val docitem_antiquotation_parser = (Scan.lift (docitem_modes -- Args.text_input) fun pretty_docitem_antiquotation_generic cid_decl ctxt ({unchecked, define}, src ) = let val (str,pos) = Input.source_content src - val _ = check_and_mark ctxt cid_decl ({strict_checking = not unchecked}) pos str val inline = Config.get ctxt Document_Antiquotation.thy_output_display + val _ = check_and_mark ctxt cid_decl {strict_checking = not unchecked} + {inline = inline} pos str val enc = Latex.enclose_block in (case (define,inline) of @@ -1683,8 +1675,6 @@ fun read_fields raw_fields ctxt = let val Ts = Syntax.read_typs ctxt (map (fn ((_, raw_T, _),_) => raw_T) raw_fields); val terms = map ((map_option (Syntax.read_term ctxt)) o snd) raw_fields - val count = Unsynchronized.ref (0 - 1); - fun incr () = Unsynchronized.inc count fun test t1 t2 = Sign.typ_instance (Proof_Context.theory_of ctxt) (t1, ODL_Command_Parser.generalize_typ 0 t2) fun check_default (ty,SOME trm) = @@ -1750,7 +1740,7 @@ fun add_doc_class_cmd overloaded (raw_params, binding) fun check_n_filter thy (bind,ty,mf) = case DOF_core.get_attribute_info parent_cid_long (Binding.name_of bind) thy of NONE => (* no prior declaration *) SOME(bind,ty,mf) - | SOME{def_occurrence,long_name,typ,def_pos} => if ty = typ + | SOME{def_occurrence,long_name,typ,...} => if ty = typ then (warning("overriding attribute:"^long_name^ " in doc class:" ^ def_occurrence); SOME(bind,ty,mf)) diff --git a/src/tests/OutOfOrderPresntn.thy b/src/tests/OutOfOrderPresntn.thy index 0145868..3335a4f 100644 --- a/src/tests/OutOfOrderPresntn.thy +++ b/src/tests/OutOfOrderPresntn.thy @@ -69,7 +69,9 @@ fun gen_enriched_document_command2 cid_transform attr_transform (* ... generating the level-attribute syntax *) in - ( ODL_Command_Parser.create_and_check_docitem false oid pos (cid_transform cid_pos) (attr_transform doc_attrs) + ( ODL_Command_Parser.create_and_check_docitem + {is_monitor = false} {is_inline = false} + oid pos (cid_transform cid_pos) (attr_transform doc_attrs) #> check_n_tex_text ) end; @@ -85,6 +87,11 @@ text\And here a tex - text macro.\ text-[dfgdfg::B]\ Lorem ipsum ... @{thm refl} \ +text\... and here is its application /macro expansion: + @{B [display] "dfgdfg"}\ + + + (*<*) text\Final Status:\ print_doc_items From 7e2224859e0f3975db156805c0a15f285e0caec8 Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Mon, 22 Jun 2020 17:42:40 +0200 Subject: [PATCH 4/4] mmm --- .ci/Jenkinsfile | 0 .ci/isabelle4isadof/Dockerfile | 0 .config | 0 .gitattributes | 0 .gitignore | 0 CHANGELOG.md | 0 CITATION | 0 LICENSE | 0 README.md | 0 ROOTS | 0 examples/CENELEC_50128/ROOTS | 0 examples/CENELEC_50128/mini_odo/ROOT | 0 .../document/figures/df-numerics-encshaft.png | Bin .../mini_odo/document/figures/odometer.jpeg | Bin .../mini_odo/document/figures/three-phase-odo.pdf | Bin .../mini_odo/document/figures/wheel-df.png | Bin examples/CENELEC_50128/mini_odo/document/isadof.cfg | 0 .../CENELEC_50128/mini_odo/document/lstisadof.sty | 0 .../CENELEC_50128/mini_odo/document/preamble.tex | 0 examples/CENELEC_50128/mini_odo/document/root.bib | 0 examples/CENELEC_50128/mini_odo/document/root.mst | 0 examples/CENELEC_50128/mini_odo/mini_odo.thy | 0 examples/README.md | 0 examples/ROOTS | 0 examples/math_exam/MathExam/MathExam.thy | 0 examples/math_exam/MathExam/ROOT | 0 .../MathExam/document/figures/Polynomialdeg5.png | Bin examples/math_exam/MathExam/document/isadof.cfg | 0 examples/math_exam/MathExam/document/preamble.tex | 0 examples/math_exam/ROOTS | 0 .../IsaDofApplications.thy | 0 .../2018-cicm-isabelle_dof-applications/ROOT | 0 .../document/figures/Dogfood-II-bgnd1.png | Bin .../figures/Dogfood-III-bgnd-text_section.png | Bin .../document/figures/Dogfood-IV-jumpInDocCLass.png | Bin .../document/figures/Dogfood-Intro.png | Bin .../document/figures/Dogfood-V-attribute.png | Bin .../document/figures/Dogfood-figures.png | Bin .../document/figures/InteractiveMathSheet.png | Bin .../document/figures/antiquotations-PIDE.png | Bin .../document/figures/isabelle-architecture.pdf | Bin .../document/figures/isabelle-architecture.svg | 0 .../document/figures/srac-as-es-application.png | Bin .../document/figures/srac-definition.png | Bin .../document/isadof.cfg | 0 .../document/lstisadof.sty | 0 .../document/preamble.tex | 0 .../document/root.bib | 0 examples/scholarly_paper/ROOTS | 0 .../Isabelle_DOF-Manual/00_Frontmatter.thy | 0 .../Isabelle_DOF-Manual/01_Introduction.thy | 0 .../Isabelle_DOF-Manual/02_Background.thy | 0 .../Isabelle_DOF-Manual/03_GuidedTour.thy | 0 .../Isabelle_DOF-Manual/04_RefMan.thy | 0 .../Isabelle_DOF-Manual/05_Implementation.thy | 0 .../Isabelle_DOF-Manual/Isabelle_DOF-Manual.thy | 0 examples/technical_report/Isabelle_DOF-Manual/ROOT | 0 .../document/figures/Dogfood-II-bgnd1.png | Bin .../figures/Dogfood-III-bgnd-text_section.png | Bin .../document/figures/Dogfood-IV-jumpInDocCLass.png | Bin .../document/figures/Dogfood-Intro.png | Bin .../document/figures/Dogfood-V-attribute.png | Bin .../document/figures/Dogfood-figures.png | Bin .../document/figures/Isabelle_DOF-logo.pdf | Bin .../document/figures/antiquotations-PIDE.png | Bin .../document/figures/cicm2018-combined.png | Bin .../document/figures/cicm2018-dof.png | Bin .../document/figures/cicm2018-pdf.png | Bin .../document/figures/document-hierarchy.pdf | Bin .../document/figures/document-hierarchy.svg | 0 .../document/figures/isabelle-architecture.pdf | Bin .../document/figures/isabelle-architecture.svg | 0 .../Isabelle_DOF-Manual/document/figures/isadof.png | Bin .../document/figures/srac-as-es-application.png | Bin .../document/figures/srac-definition.png | Bin .../Isabelle_DOF-Manual/document/isadof.cfg | 0 .../document/lstisadof-manual.sty | 0 .../Isabelle_DOF-Manual/document/preamble.tex | 0 .../Isabelle_DOF-Manual/document/root.bib | 0 .../Isabelle_DOF-Manual/document/root.mst | 0 examples/technical_report/ROOTS | 0 .../technical_report/TR_my_commented_isabelle/ROOT | 0 .../TR_MyCommentedIsabelle.thy | 0 .../document/figures/document-model.pdf | Bin .../document/figures/isabelle-architecture.pdf | Bin .../document/figures/markup-demo.png | Bin .../document/figures/pure-inferences-I.pdf | Bin .../document/figures/pure-inferences-II.pdf | Bin .../document/figures/text-element.pdf | Bin .../TR_my_commented_isabelle/document/isadof.cfg | 0 .../TR_my_commented_isabelle/document/preamble.tex | 0 .../TR_my_commented_isabelle/document/prooftree.sty | 0 .../TR_my_commented_isabelle/document/root.bib | 0 src/DOF/Assert.thy | 0 src/DOF/AssertLong.thy | 0 src/DOF/Isa_COL.thy | 0 src/DOF/Isa_DOF.thy | 0 src/DOF/RegExpInterface.thy | 0 src/DOF/latex/DOF-COL.sty | 0 src/DOF/latex/DOF-core.sty | 0 src/ROOT | 0 src/ROOTS | 0 src/SI/Groups_mult.thy | 0 src/SI/ISQ.thy | 0 src/SI/ISQ_Algebra.thy | 0 src/SI/ISQ_Dimensions.thy | 0 src/SI/ISQ_Proof.thy | 0 src/SI/ISQ_Quantities.thy | 0 src/SI/ROOT | 0 src/SI/SI.thy | 0 src/SI/SIOld.thy | 0 src/SI/SI_Accepted.thy | 0 src/SI/SI_Astronomical.thy | 0 src/SI/SI_Constants.thy | 0 src/SI/SI_Derived.thy | 0 src/SI/SI_Imperial.thy | 0 src/SI/SI_Prefix.thy | 0 src/SI/SI_Units.thy | 0 src/SI/document/adb-long.bib | 0 src/SI/document/root.bib | 0 src/SI/document/root.tex | 0 src/document-templates/root-eptcs-UNSUPPORTED.tex | 0 .../root-lipics-v2019-UNSUPPORTED.tex | 0 src/document-templates/root-lncs.tex | 0 src/document-templates/root-scrartcl.tex | 0 src/document-templates/root-scrreprt-modern.tex | 0 src/document-templates/root-scrreprt.tex | 0 src/ontologies/CENELEC_50128/CENELEC_50128.thy | 0 src/ontologies/CENELEC_50128/DOF-CENELEC_50128.sty | 0 src/ontologies/Conceptual/Conceptual.thy | 0 src/ontologies/math_exam/DOF-math_exam.sty | 0 src/ontologies/math_exam/Nmath_exam.thy | 0 src/ontologies/math_exam/math_exam.thy | 0 src/ontologies/math_paper/math_paper.thy | 0 src/ontologies/ontologies.thy | 0 .../scholarly_paper/DOF-scholarly_paper.sty | 0 src/ontologies/scholarly_paper/scholarly_paper.thy | 0 src/ontologies/small_math/small_math.thy | 0 .../technical_report/DOF-technical_report.sty | 0 .../technical_report/technical_report.thy | 0 src/patches/thy_output.Isabelle2020.ML | 0 src/patches/thy_output.ML | 0 src/tests/AssnsLemmaThmEtc.thy | 0 src/tests/Attributes.thy | 0 src/tests/Concept_Example.thy | 0 src/tests/Concept_ExampleInvariant.thy | 0 src/tests/InnerSyntaxAntiquotations.thy | 0 src/tests/ROOT | 0 src/tests/figures/A.png | Bin src/tests/figures/AnB.odp | Bin src/tests/figures/B.png | Bin 151 files changed, 0 insertions(+), 0 deletions(-) mode change 100644 => 100755 .ci/Jenkinsfile mode change 100644 => 100755 .ci/isabelle4isadof/Dockerfile mode change 100644 => 100755 .config mode change 100644 => 100755 .gitattributes mode change 100644 => 100755 .gitignore mode change 100644 => 100755 CHANGELOG.md mode change 100644 => 100755 CITATION mode change 100644 => 100755 LICENSE mode change 100644 => 100755 README.md mode change 100644 => 100755 ROOTS mode change 100644 => 100755 examples/CENELEC_50128/ROOTS mode change 100644 => 100755 examples/CENELEC_50128/mini_odo/ROOT mode change 100644 => 100755 examples/CENELEC_50128/mini_odo/document/figures/df-numerics-encshaft.png mode change 100644 => 100755 examples/CENELEC_50128/mini_odo/document/figures/odometer.jpeg mode change 100644 => 100755 examples/CENELEC_50128/mini_odo/document/figures/three-phase-odo.pdf mode change 100644 => 100755 examples/CENELEC_50128/mini_odo/document/figures/wheel-df.png mode change 100644 => 100755 examples/CENELEC_50128/mini_odo/document/isadof.cfg mode change 100644 => 100755 examples/CENELEC_50128/mini_odo/document/lstisadof.sty mode change 100644 => 100755 examples/CENELEC_50128/mini_odo/document/preamble.tex mode change 100644 => 100755 examples/CENELEC_50128/mini_odo/document/root.bib mode change 100644 => 100755 examples/CENELEC_50128/mini_odo/document/root.mst mode change 100644 => 100755 examples/CENELEC_50128/mini_odo/mini_odo.thy mode change 100644 => 100755 examples/README.md mode change 100644 => 100755 examples/ROOTS mode change 100644 => 100755 examples/math_exam/MathExam/MathExam.thy mode change 100644 => 100755 examples/math_exam/MathExam/ROOT mode change 100644 => 100755 examples/math_exam/MathExam/document/figures/Polynomialdeg5.png mode change 100644 => 100755 examples/math_exam/MathExam/document/isadof.cfg mode change 100644 => 100755 examples/math_exam/MathExam/document/preamble.tex mode change 100644 => 100755 examples/math_exam/ROOTS mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/ROOT mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-II-bgnd1.png mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-III-bgnd-text_section.png mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-IV-jumpInDocCLass.png mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-Intro.png mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-V-attribute.png mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-figures.png mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/InteractiveMathSheet.png mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/antiquotations-PIDE.png mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/isabelle-architecture.pdf mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/isabelle-architecture.svg mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/srac-as-es-application.png mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/srac-definition.png mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/isadof.cfg mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/lstisadof.sty mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/preamble.tex mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/root.bib mode change 100644 => 100755 examples/scholarly_paper/ROOTS mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/02_Background.thy mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/Isabelle_DOF-Manual.thy mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/ROOT mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-II-bgnd1.png mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-III-bgnd-text_section.png mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-IV-jumpInDocCLass.png mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-Intro.png mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-V-attribute.png mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-figures.png mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/Isabelle_DOF-logo.pdf mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/antiquotations-PIDE.png mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-combined.png mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-dof.png mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-pdf.png mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/document-hierarchy.pdf mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/document-hierarchy.svg mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/isabelle-architecture.pdf mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/isabelle-architecture.svg mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/isadof.png mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/srac-as-es-application.png mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/srac-definition.png mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/isadof.cfg mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/lstisadof-manual.sty mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/root.bib mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/root.mst mode change 100644 => 100755 examples/technical_report/ROOTS mode change 100644 => 100755 examples/technical_report/TR_my_commented_isabelle/ROOT mode change 100644 => 100755 examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy mode change 100644 => 100755 examples/technical_report/TR_my_commented_isabelle/document/figures/document-model.pdf mode change 100644 => 100755 examples/technical_report/TR_my_commented_isabelle/document/figures/isabelle-architecture.pdf mode change 100644 => 100755 examples/technical_report/TR_my_commented_isabelle/document/figures/markup-demo.png mode change 100644 => 100755 examples/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-I.pdf mode change 100644 => 100755 examples/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-II.pdf mode change 100644 => 100755 examples/technical_report/TR_my_commented_isabelle/document/figures/text-element.pdf mode change 100644 => 100755 examples/technical_report/TR_my_commented_isabelle/document/isadof.cfg mode change 100644 => 100755 examples/technical_report/TR_my_commented_isabelle/document/preamble.tex mode change 100644 => 100755 examples/technical_report/TR_my_commented_isabelle/document/prooftree.sty mode change 100644 => 100755 examples/technical_report/TR_my_commented_isabelle/document/root.bib mode change 100644 => 100755 src/DOF/Assert.thy mode change 100644 => 100755 src/DOF/AssertLong.thy mode change 100644 => 100755 src/DOF/Isa_COL.thy mode change 100644 => 100755 src/DOF/Isa_DOF.thy mode change 100644 => 100755 src/DOF/RegExpInterface.thy mode change 100644 => 100755 src/DOF/latex/DOF-COL.sty mode change 100644 => 100755 src/DOF/latex/DOF-core.sty mode change 100644 => 100755 src/ROOT mode change 100644 => 100755 src/ROOTS mode change 100644 => 100755 src/SI/Groups_mult.thy mode change 100644 => 100755 src/SI/ISQ.thy mode change 100644 => 100755 src/SI/ISQ_Algebra.thy mode change 100644 => 100755 src/SI/ISQ_Dimensions.thy mode change 100644 => 100755 src/SI/ISQ_Proof.thy mode change 100644 => 100755 src/SI/ISQ_Quantities.thy mode change 100644 => 100755 src/SI/ROOT mode change 100644 => 100755 src/SI/SI.thy mode change 100644 => 100755 src/SI/SIOld.thy mode change 100644 => 100755 src/SI/SI_Accepted.thy mode change 100644 => 100755 src/SI/SI_Astronomical.thy mode change 100644 => 100755 src/SI/SI_Constants.thy mode change 100644 => 100755 src/SI/SI_Derived.thy mode change 100644 => 100755 src/SI/SI_Imperial.thy mode change 100644 => 100755 src/SI/SI_Prefix.thy mode change 100644 => 100755 src/SI/SI_Units.thy mode change 100644 => 100755 src/SI/document/adb-long.bib mode change 100644 => 100755 src/SI/document/root.bib mode change 100644 => 100755 src/SI/document/root.tex mode change 100644 => 100755 src/document-templates/root-eptcs-UNSUPPORTED.tex mode change 100644 => 100755 src/document-templates/root-lipics-v2019-UNSUPPORTED.tex mode change 100644 => 100755 src/document-templates/root-lncs.tex mode change 100644 => 100755 src/document-templates/root-scrartcl.tex mode change 100644 => 100755 src/document-templates/root-scrreprt-modern.tex mode change 100644 => 100755 src/document-templates/root-scrreprt.tex mode change 100644 => 100755 src/ontologies/CENELEC_50128/CENELEC_50128.thy mode change 100644 => 100755 src/ontologies/CENELEC_50128/DOF-CENELEC_50128.sty mode change 100644 => 100755 src/ontologies/Conceptual/Conceptual.thy mode change 100644 => 100755 src/ontologies/math_exam/DOF-math_exam.sty mode change 100644 => 100755 src/ontologies/math_exam/Nmath_exam.thy mode change 100644 => 100755 src/ontologies/math_exam/math_exam.thy mode change 100644 => 100755 src/ontologies/math_paper/math_paper.thy mode change 100644 => 100755 src/ontologies/ontologies.thy mode change 100644 => 100755 src/ontologies/scholarly_paper/DOF-scholarly_paper.sty mode change 100644 => 100755 src/ontologies/scholarly_paper/scholarly_paper.thy mode change 100644 => 100755 src/ontologies/small_math/small_math.thy mode change 100644 => 100755 src/ontologies/technical_report/DOF-technical_report.sty mode change 100644 => 100755 src/ontologies/technical_report/technical_report.thy mode change 100644 => 100755 src/patches/thy_output.Isabelle2020.ML mode change 100644 => 100755 src/patches/thy_output.ML mode change 100644 => 100755 src/tests/AssnsLemmaThmEtc.thy mode change 100644 => 100755 src/tests/Attributes.thy mode change 100644 => 100755 src/tests/Concept_Example.thy mode change 100644 => 100755 src/tests/Concept_ExampleInvariant.thy mode change 100644 => 100755 src/tests/InnerSyntaxAntiquotations.thy mode change 100644 => 100755 src/tests/ROOT mode change 100644 => 100755 src/tests/figures/A.png mode change 100644 => 100755 src/tests/figures/AnB.odp mode change 100644 => 100755 src/tests/figures/B.png diff --git a/.ci/Jenkinsfile b/.ci/Jenkinsfile old mode 100644 new mode 100755 diff --git a/.ci/isabelle4isadof/Dockerfile b/.ci/isabelle4isadof/Dockerfile old mode 100644 new mode 100755 diff --git a/.config b/.config old mode 100644 new mode 100755 diff --git a/.gitattributes b/.gitattributes old mode 100644 new mode 100755 diff --git a/.gitignore b/.gitignore old mode 100644 new mode 100755 diff --git a/CHANGELOG.md b/CHANGELOG.md old mode 100644 new mode 100755 diff --git a/CITATION b/CITATION old mode 100644 new mode 100755 diff --git a/LICENSE b/LICENSE old mode 100644 new mode 100755 diff --git a/README.md b/README.md old mode 100644 new mode 100755 diff --git a/ROOTS b/ROOTS old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/ROOTS b/examples/CENELEC_50128/ROOTS old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/mini_odo/ROOT b/examples/CENELEC_50128/mini_odo/ROOT old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/mini_odo/document/figures/df-numerics-encshaft.png b/examples/CENELEC_50128/mini_odo/document/figures/df-numerics-encshaft.png old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/mini_odo/document/figures/odometer.jpeg b/examples/CENELEC_50128/mini_odo/document/figures/odometer.jpeg old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/mini_odo/document/figures/three-phase-odo.pdf b/examples/CENELEC_50128/mini_odo/document/figures/three-phase-odo.pdf old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/mini_odo/document/figures/wheel-df.png b/examples/CENELEC_50128/mini_odo/document/figures/wheel-df.png old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/mini_odo/document/isadof.cfg b/examples/CENELEC_50128/mini_odo/document/isadof.cfg old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/mini_odo/document/lstisadof.sty b/examples/CENELEC_50128/mini_odo/document/lstisadof.sty old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/mini_odo/document/preamble.tex b/examples/CENELEC_50128/mini_odo/document/preamble.tex old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/mini_odo/document/root.bib b/examples/CENELEC_50128/mini_odo/document/root.bib old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/mini_odo/document/root.mst b/examples/CENELEC_50128/mini_odo/document/root.mst old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/mini_odo/mini_odo.thy b/examples/CENELEC_50128/mini_odo/mini_odo.thy old mode 100644 new mode 100755 diff --git a/examples/README.md b/examples/README.md old mode 100644 new mode 100755 diff --git a/examples/ROOTS b/examples/ROOTS old mode 100644 new mode 100755 diff --git a/examples/math_exam/MathExam/MathExam.thy b/examples/math_exam/MathExam/MathExam.thy old mode 100644 new mode 100755 diff --git a/examples/math_exam/MathExam/ROOT b/examples/math_exam/MathExam/ROOT old mode 100644 new mode 100755 diff --git a/examples/math_exam/MathExam/document/figures/Polynomialdeg5.png b/examples/math_exam/MathExam/document/figures/Polynomialdeg5.png old mode 100644 new mode 100755 diff --git a/examples/math_exam/MathExam/document/isadof.cfg b/examples/math_exam/MathExam/document/isadof.cfg old mode 100644 new mode 100755 diff --git a/examples/math_exam/MathExam/document/preamble.tex b/examples/math_exam/MathExam/document/preamble.tex old mode 100644 new mode 100755 diff --git a/examples/math_exam/ROOTS b/examples/math_exam/ROOTS old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/ROOT b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/ROOT old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-II-bgnd1.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-II-bgnd1.png old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-III-bgnd-text_section.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-III-bgnd-text_section.png old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-IV-jumpInDocCLass.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-IV-jumpInDocCLass.png old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-Intro.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-Intro.png old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-V-attribute.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-V-attribute.png old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-figures.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-figures.png old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/InteractiveMathSheet.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/InteractiveMathSheet.png old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/antiquotations-PIDE.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/antiquotations-PIDE.png old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/isabelle-architecture.pdf b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/isabelle-architecture.pdf old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/isabelle-architecture.svg b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/isabelle-architecture.svg old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/srac-as-es-application.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/srac-as-es-application.png old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/srac-definition.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/srac-definition.png old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/isadof.cfg b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/isadof.cfg old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/lstisadof.sty b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/lstisadof.sty old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/preamble.tex b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/preamble.tex old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/root.bib b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/root.bib old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/ROOTS b/examples/scholarly_paper/ROOTS old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy b/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy b/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy b/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy b/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/Isabelle_DOF-Manual.thy b/examples/technical_report/Isabelle_DOF-Manual/Isabelle_DOF-Manual.thy old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/ROOT b/examples/technical_report/Isabelle_DOF-Manual/ROOT old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-II-bgnd1.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-II-bgnd1.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-III-bgnd-text_section.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-III-bgnd-text_section.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-IV-jumpInDocCLass.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-IV-jumpInDocCLass.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-Intro.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-Intro.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-V-attribute.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-V-attribute.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-figures.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-figures.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Isabelle_DOF-logo.pdf b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Isabelle_DOF-logo.pdf old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/antiquotations-PIDE.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/antiquotations-PIDE.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-combined.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-combined.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-dof.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-dof.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-pdf.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-pdf.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/document-hierarchy.pdf b/examples/technical_report/Isabelle_DOF-Manual/document/figures/document-hierarchy.pdf old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/document-hierarchy.svg b/examples/technical_report/Isabelle_DOF-Manual/document/figures/document-hierarchy.svg old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/isabelle-architecture.pdf b/examples/technical_report/Isabelle_DOF-Manual/document/figures/isabelle-architecture.pdf old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/isabelle-architecture.svg b/examples/technical_report/Isabelle_DOF-Manual/document/figures/isabelle-architecture.svg old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/isadof.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/isadof.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/srac-as-es-application.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/srac-as-es-application.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/srac-definition.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/srac-definition.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/isadof.cfg b/examples/technical_report/Isabelle_DOF-Manual/document/isadof.cfg old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/lstisadof-manual.sty b/examples/technical_report/Isabelle_DOF-Manual/document/lstisadof-manual.sty old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex b/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/root.bib b/examples/technical_report/Isabelle_DOF-Manual/document/root.bib old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/root.mst b/examples/technical_report/Isabelle_DOF-Manual/document/root.mst old mode 100644 new mode 100755 diff --git a/examples/technical_report/ROOTS b/examples/technical_report/ROOTS old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/ROOT b/examples/technical_report/TR_my_commented_isabelle/ROOT old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/figures/document-model.pdf b/examples/technical_report/TR_my_commented_isabelle/document/figures/document-model.pdf old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/figures/isabelle-architecture.pdf b/examples/technical_report/TR_my_commented_isabelle/document/figures/isabelle-architecture.pdf old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/figures/markup-demo.png b/examples/technical_report/TR_my_commented_isabelle/document/figures/markup-demo.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-I.pdf b/examples/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-I.pdf old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-II.pdf b/examples/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-II.pdf old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/figures/text-element.pdf b/examples/technical_report/TR_my_commented_isabelle/document/figures/text-element.pdf old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/isadof.cfg b/examples/technical_report/TR_my_commented_isabelle/document/isadof.cfg old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/preamble.tex b/examples/technical_report/TR_my_commented_isabelle/document/preamble.tex old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/prooftree.sty b/examples/technical_report/TR_my_commented_isabelle/document/prooftree.sty old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/root.bib b/examples/technical_report/TR_my_commented_isabelle/document/root.bib old mode 100644 new mode 100755 diff --git a/src/DOF/Assert.thy b/src/DOF/Assert.thy old mode 100644 new mode 100755 diff --git a/src/DOF/AssertLong.thy b/src/DOF/AssertLong.thy old mode 100644 new mode 100755 diff --git a/src/DOF/Isa_COL.thy b/src/DOF/Isa_COL.thy old mode 100644 new mode 100755 diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy old mode 100644 new mode 100755 diff --git a/src/DOF/RegExpInterface.thy b/src/DOF/RegExpInterface.thy old mode 100644 new mode 100755 diff --git a/src/DOF/latex/DOF-COL.sty b/src/DOF/latex/DOF-COL.sty old mode 100644 new mode 100755 diff --git a/src/DOF/latex/DOF-core.sty b/src/DOF/latex/DOF-core.sty old mode 100644 new mode 100755 diff --git a/src/ROOT b/src/ROOT old mode 100644 new mode 100755 diff --git a/src/ROOTS b/src/ROOTS old mode 100644 new mode 100755 diff --git a/src/SI/Groups_mult.thy b/src/SI/Groups_mult.thy old mode 100644 new mode 100755 diff --git a/src/SI/ISQ.thy b/src/SI/ISQ.thy old mode 100644 new mode 100755 diff --git a/src/SI/ISQ_Algebra.thy b/src/SI/ISQ_Algebra.thy old mode 100644 new mode 100755 diff --git a/src/SI/ISQ_Dimensions.thy b/src/SI/ISQ_Dimensions.thy old mode 100644 new mode 100755 diff --git a/src/SI/ISQ_Proof.thy b/src/SI/ISQ_Proof.thy old mode 100644 new mode 100755 diff --git a/src/SI/ISQ_Quantities.thy b/src/SI/ISQ_Quantities.thy old mode 100644 new mode 100755 diff --git a/src/SI/ROOT b/src/SI/ROOT old mode 100644 new mode 100755 diff --git a/src/SI/SI.thy b/src/SI/SI.thy old mode 100644 new mode 100755 diff --git a/src/SI/SIOld.thy b/src/SI/SIOld.thy old mode 100644 new mode 100755 diff --git a/src/SI/SI_Accepted.thy b/src/SI/SI_Accepted.thy old mode 100644 new mode 100755 diff --git a/src/SI/SI_Astronomical.thy b/src/SI/SI_Astronomical.thy old mode 100644 new mode 100755 diff --git a/src/SI/SI_Constants.thy b/src/SI/SI_Constants.thy old mode 100644 new mode 100755 diff --git a/src/SI/SI_Derived.thy b/src/SI/SI_Derived.thy old mode 100644 new mode 100755 diff --git a/src/SI/SI_Imperial.thy b/src/SI/SI_Imperial.thy old mode 100644 new mode 100755 diff --git a/src/SI/SI_Prefix.thy b/src/SI/SI_Prefix.thy old mode 100644 new mode 100755 diff --git a/src/SI/SI_Units.thy b/src/SI/SI_Units.thy old mode 100644 new mode 100755 diff --git a/src/SI/document/adb-long.bib b/src/SI/document/adb-long.bib old mode 100644 new mode 100755 diff --git a/src/SI/document/root.bib b/src/SI/document/root.bib old mode 100644 new mode 100755 diff --git a/src/SI/document/root.tex b/src/SI/document/root.tex old mode 100644 new mode 100755 diff --git a/src/document-templates/root-eptcs-UNSUPPORTED.tex b/src/document-templates/root-eptcs-UNSUPPORTED.tex old mode 100644 new mode 100755 diff --git a/src/document-templates/root-lipics-v2019-UNSUPPORTED.tex b/src/document-templates/root-lipics-v2019-UNSUPPORTED.tex old mode 100644 new mode 100755 diff --git a/src/document-templates/root-lncs.tex b/src/document-templates/root-lncs.tex old mode 100644 new mode 100755 diff --git a/src/document-templates/root-scrartcl.tex b/src/document-templates/root-scrartcl.tex old mode 100644 new mode 100755 diff --git a/src/document-templates/root-scrreprt-modern.tex b/src/document-templates/root-scrreprt-modern.tex old mode 100644 new mode 100755 diff --git a/src/document-templates/root-scrreprt.tex b/src/document-templates/root-scrreprt.tex old mode 100644 new mode 100755 diff --git a/src/ontologies/CENELEC_50128/CENELEC_50128.thy b/src/ontologies/CENELEC_50128/CENELEC_50128.thy old mode 100644 new mode 100755 diff --git a/src/ontologies/CENELEC_50128/DOF-CENELEC_50128.sty b/src/ontologies/CENELEC_50128/DOF-CENELEC_50128.sty old mode 100644 new mode 100755 diff --git a/src/ontologies/Conceptual/Conceptual.thy b/src/ontologies/Conceptual/Conceptual.thy old mode 100644 new mode 100755 diff --git a/src/ontologies/math_exam/DOF-math_exam.sty b/src/ontologies/math_exam/DOF-math_exam.sty old mode 100644 new mode 100755 diff --git a/src/ontologies/math_exam/Nmath_exam.thy b/src/ontologies/math_exam/Nmath_exam.thy old mode 100644 new mode 100755 diff --git a/src/ontologies/math_exam/math_exam.thy b/src/ontologies/math_exam/math_exam.thy old mode 100644 new mode 100755 diff --git a/src/ontologies/math_paper/math_paper.thy b/src/ontologies/math_paper/math_paper.thy old mode 100644 new mode 100755 diff --git a/src/ontologies/ontologies.thy b/src/ontologies/ontologies.thy old mode 100644 new mode 100755 diff --git a/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty b/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty old mode 100644 new mode 100755 diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy old mode 100644 new mode 100755 diff --git a/src/ontologies/small_math/small_math.thy b/src/ontologies/small_math/small_math.thy old mode 100644 new mode 100755 diff --git a/src/ontologies/technical_report/DOF-technical_report.sty b/src/ontologies/technical_report/DOF-technical_report.sty old mode 100644 new mode 100755 diff --git a/src/ontologies/technical_report/technical_report.thy b/src/ontologies/technical_report/technical_report.thy old mode 100644 new mode 100755 diff --git a/src/patches/thy_output.Isabelle2020.ML b/src/patches/thy_output.Isabelle2020.ML old mode 100644 new mode 100755 diff --git a/src/patches/thy_output.ML b/src/patches/thy_output.ML old mode 100644 new mode 100755 diff --git a/src/tests/AssnsLemmaThmEtc.thy b/src/tests/AssnsLemmaThmEtc.thy old mode 100644 new mode 100755 diff --git a/src/tests/Attributes.thy b/src/tests/Attributes.thy old mode 100644 new mode 100755 diff --git a/src/tests/Concept_Example.thy b/src/tests/Concept_Example.thy old mode 100644 new mode 100755 diff --git a/src/tests/Concept_ExampleInvariant.thy b/src/tests/Concept_ExampleInvariant.thy old mode 100644 new mode 100755 diff --git a/src/tests/InnerSyntaxAntiquotations.thy b/src/tests/InnerSyntaxAntiquotations.thy old mode 100644 new mode 100755 diff --git a/src/tests/ROOT b/src/tests/ROOT old mode 100644 new mode 100755 diff --git a/src/tests/figures/A.png b/src/tests/figures/A.png old mode 100644 new mode 100755 diff --git a/src/tests/figures/AnB.odp b/src/tests/figures/AnB.odp old mode 100644 new mode 100755 diff --git a/src/tests/figures/B.png b/src/tests/figures/B.png old mode 100644 new mode 100755