pierre.derathe
/
Isabelle_DOF
Archived
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Commit Graph

  • 244d70896f Merge branch 'main' into test-rebase2 common-criteria Pierre Derathe 2023-02-20 12:20:07 +0100
  • ba0e7d25d3 Common_Criteria_Tests finished with current fonctionnalities Pierre Derathe 2023-01-25 16:47:53 +0100
  • 57bd44ecde Enable build for Common_Criteria ontology Pierre Derathe 2023-01-25 15:45:37 +0100
  • 983f4cf1c4 Add Common Criteria Terms Pierre Derathe 2023-02-20 11:26:01 +0100
  • 55ff33df17 Referencing term in cc_tests Pierre Derathe 2023-02-20 10:28:04 +0100
  • ec81f7bbce Final version Pierre Derathe 2023-02-19 16:26:23 +0100
  • 2f4307a907 Merge branch 'common-criteria' of https://git.logicalhacking.com/pierre.derathe/Isabelle_DOF into common-criteria Pierre Derathe 2023-02-19 16:14:10 +0100
  • d67e270b3d Change of cc and cc_test to be used to create a pdf Pierre Derathe 2023-02-19 16:08:37 +0100
  • 848ce311e2 Re-add name field to onto_class Nicolas Méric 2023-02-17 12:56:45 +0100
  • 6115f0de4a Some cleanup Nicolas Méric 2023-02-17 11:35:51 +0100
  • bdfea3ddb1 Some cleanup Nicolas Méric 2023-02-17 09:08:34 +0100
  • 9de18b148a Remove some instance and onto_class datatypes entries Nicolas Méric 2023-02-16 10:41:04 +0100
  • 1459b8cfc3 Use name space markup for onto_class entries reporting Nicolas Méric 2023-02-16 10:07:56 +0100
  • 234ff18ec0 Use a name space for Onto Classes Nicolas Méric 2023-02-14 17:57:53 +0100
  • 55690bba33 Homogenize instance getters names Nicolas Méric 2023-02-14 07:39:06 +0100
  • 93509ab17d Update file to match the new name space implementation Nicolas Méric 2023-02-14 07:09:27 +0100
  • 1e09598d81 Fix typo Nicolas Méric 2023-02-14 07:08:43 +0100
  • e01ec9fc21 Use a name space for ML invariants Nicolas Méric 2023-02-12 17:57:35 +0100
  • 7c16d02979 Use a name space for Isabelle_DOF transformers Nicolas Méric 2023-02-12 15:56:06 +0100
  • 4a77347e40 Simplify reporting of monitors Nicolas Méric 2023-02-12 11:16:07 +0100
  • 2398fc579a Use name space markup for instances entries reporting Nicolas Méric 2023-02-11 22:48:11 +0100
  • 821eefb230 Fix some markups Nicolas Méric 2023-02-10 15:23:23 +0100
  • 9b51844fad Use a name space for monitors infos Nicolas Méric 2023-02-09 16:41:32 +0100
  • c440f9628f Fix typo Nicolas Méric 2023-02-09 16:40:05 +0100
  • 5b3086bbe5 Use a name space for docitems (instances) Nicolas Méric 2023-02-06 17:09:02 +0100
  • 5aaa5451f6 Common_Criteria_Tests finished with current fonctionnalities Pierre Derathe 2023-01-25 16:47:53 +0100
  • 1d4211d7c4 Enable build for Common_Criteria ontology Pierre Derathe 2023-01-25 15:45:37 +0100
  • fcae04fd83 Modify CC, CC_tests and CC_terms Pierre Derathe 2023-01-25 14:47:03 +0100
  • fab3b3394e Add Common Criteria ontology first draft Pierre Derathe 2023-01-18 18:19:47 +0100
  • 7c0d2cee55 Add docitem_name text and ML antiquotations Nicolas Méric 2023-01-30 07:43:44 +0100
  • 7c6150affa Make input_term available with theory option Nicolas Méric 2023-01-27 15:06:20 +0100
  • ad4ad52b4e Avoid reporting duplication when possible Nicolas Méric 2023-01-27 10:32:38 +0100
  • ba8227e6ab Cleanup and add position to docitem ML antiqutation Nicolas Méric 2023-01-26 09:43:51 +0100
  • a75c47d6b6 Common_Criteria_Tests finished with current fonctionnalities Pierre Derathe 2023-01-25 16:47:53 +0100
  • 997491d61f Enable build for Common_Criteria ontology Pierre Derathe 2023-01-25 15:45:37 +0100
  • 58edd373f0 Modify CC, CC_tests and CC_terms Pierre Derathe 2023-01-25 14:47:03 +0100
  • 4d51d407c6 Add Common Criteria ontology first draft Pierre Derathe 2023-01-18 18:19:47 +0100
  • 20b0af740d Update meta args syntax and ML* command Nicolas Méric 2023-01-23 08:50:36 +0100
  • 1379f8a671 Add test of invariants of an inherited attribute of an attribute Nicolas Méric 2023-01-18 19:11:48 +0100
  • 8fdaafa295 Experimental session with enabled proof objects: Isabelle_DOF-Proofs. Achim D. Brucker 2023-01-19 22:00:53 +0000
  • 756f2b66f1 Add very deep interpretation metalogic-mapping-2 Nicolas Méric 2023-01-16 15:52:23 +0100
  • 5d2a0c1ff4 Update file hierarchy with Bu proposition metalogic-mapping Nicolas Méric 2023-01-16 14:45:25 +0100
  • 196c57799f Make both deep and shallow interpretation available Nicolas Méric 2023-01-13 12:38:15 +0100
  • f372eee9df Update file hierarchy for meta-interpretation Nicolas Méric 2022-12-21 18:26:11 +0100
  • 3fb0aaf3ee Add examples to choose between proof_of and prop Nicolas Méric 2022-12-05 19:16:18 +0100
  • 50a41bbcdd Add metalogic handling Nicolas Méric 2022-07-08 08:13:46 +0200
  • 8513f7d267 Update doc_class rails to match accepts clause main Nicolas Méric 2023-01-17 09:01:55 +0100
  • 2b1a9d009e Add support invariants on attributes of attributes Nicolas Méric 2023-01-13 08:23:15 +0100
  • cd758d2c44 Update accepts clause syntax Nicolas Méric 2023-01-12 12:18:58 +0100
  • 8496963fec Add comment for term_ and value_ ML antiquoatations Nicolas Méric 2023-01-11 14:49:29 +0100
  • 72d8000f7b Further explain evaluator option syntax for value_ text antiquotation Nicolas Méric 2023-01-09 15:34:59 +0100
  • 17ec11b297 Explain evaluator option syntax for value_ text antiquotation Nicolas Méric 2023-01-09 15:13:23 +0100
  • a96e17abf3 Add term_ and value_ ML antiquotations Nicolas Méric 2023-01-09 11:34:40 +0100
  • 74b60e47d5 Document term _ and value_ text antiquotations Nicolas Méric 2022-12-22 16:36:49 +0100
  • a42dd4ea6c Implement term _ and value_ text antiquotations Nicolas Méric 2022-12-22 10:55:03 +0100
  • b162a24749 Comment out hack for Assumption in scholarly_paper Nicolas Méric 2022-12-22 09:55:46 +0100
  • a9432c7b52 Add a theory attribute to disable invariants checking Nicolas Méric 2022-12-22 07:53:42 +0100
  • 9f28d4949e Limit scope of free class checking in examples Nicolas Méric 2022-12-22 07:32:37 +0100
  • 885c23a138 Explain lazy and eager invariants Nicolas Méric 2022-12-22 07:14:29 +0100
  • a589d4cd47 Update the position of the default class Nicolas Méric 2022-12-21 18:32:07 +0100
  • e1f143d151 Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF Burkhart Wolff 2022-12-21 11:35:05 +0100
  • fd60cf2312 attempt to add category 'assumption' Burkhart Wolff 2022-12-21 11:34:34 +0100
  • 73dfcd6c1e Implement rejects clause Nicolas Méric 2022-12-14 12:02:15 +0100
  • c0afe1105e Enable high-level invariants checking everywhere Nicolas Méric 2022-12-12 12:01:04 +0100
  • e414b97afb rephrasing invariant for core scholarly_paper classes Burkhart Wolff 2022-12-19 12:14:30 +0100
  • 0b2d28b547 Update error message for invariant checking Nicolas Méric 2022-12-09 16:11:57 +0100
  • 37d7ed7d17 Update rails for annotated text element in manual Nicolas Méric 2022-12-09 15:13:22 +0100
  • 312734afbd Update Attributes examples Nicolas Méric 2022-12-09 15:12:38 +0100
  • 8cee80d78e advanced example on trace-attribute term-antiquotations Burkhart Wolff 2022-12-07 16:01:38 +0100
  • ec0d525426 Tuned messages, following Isabelle/d6a2a8bc40e1 Makarius Wenzel 2022-12-05 15:21:26 +0100
  • 791990039b Tuned messages and options, following Isabelle/c7f3e94fce7b Makarius Wenzel 2022-12-05 12:37:59 +0100
  • 78d61390fe Prefer Isar command, instead of its underlying ML implementation Makarius Wenzel 2022-12-05 11:50:12 +0100
  • ffcf1f3240 Add missing file (amending 5471d873a9) Makarius Wenzel 2022-12-04 19:26:28 +0100
  • 5471d873a9 Isabelle/Scala module within session context supports document_build = "dof" without component setup Makarius Wenzel 2022-12-04 19:13:08 +0100
  • df37250a00 Simplified args, following README.md Makarius Wenzel 2022-12-04 19:00:23 +0100
  • 185daeb577 Tuned Makarius Wenzel 2022-12-04 18:25:29 +0100
  • 8037fd15f2 Tuned messages, following isabelle.Export.message Makarius Wenzel 2022-12-04 18:20:54 +0100
  • afcd78610b More concise export artifact Makarius Wenzel 2022-12-04 18:03:53 +0100
  • b8a9ef5118 Tuned comments Makarius Wenzel 2022-12-04 16:38:56 +0100
  • a4e75c8b12 Clarified export name for the sake of low-level errors Makarius Wenzel 2022-12-04 16:35:55 +0100
  • d20e9ccd22 Proper session qualifier for theory imports (amending 44cae2e631) Makarius Wenzel 2022-12-04 00:45:07 +0100
  • f2ee5d3780 Tuned Makarius Wenzel 2022-12-04 00:10:43 +0100
  • 44cae2e631 More formal management of ontologies in Isabelle/ML/Isar with output via Isabelle/Scala exports Makarius Wenzel 2022-12-04 00:09:29 +0100
  • 7b2bf35353 More strict treatment of document export artifacts Makarius Wenzel 2022-12-03 14:54:14 +0100
  • e8c7fa6018 Clarified signature Makarius Wenzel 2022-12-03 14:44:04 +0100
  • b12e61511d Discourage etc/options Makarius Wenzel 2022-12-03 13:55:56 +0100
  • 3cac42e6cb Clarified order Makarius Wenzel 2022-12-03 12:39:00 +0100
  • aee8ba1df1 Prefer DOF parameters over Isabelle options Makarius Wenzel 2022-12-03 12:37:58 +0100
  • d93e1383d4 Afford full-scale command-line tool Makarius Wenzel 2022-12-03 12:29:24 +0100
  • 3d5d1e7476 Further attempts at woodpecker environment Makarius Wenzel 2022-12-02 22:54:02 +0100
  • 4264e7cd15 Build Scala/Java components to get proper ISABELLE_CLASSPATH Makarius Wenzel 2022-12-02 21:40:59 +0100
  • 96f4077c53 Tuned message Makarius Wenzel 2022-12-02 21:29:45 +0100
  • d7fb39d7eb Adhoc command-line tool replaces old options Makarius Wenzel 2022-12-02 21:14:55 +0100
  • b95826962f Tuned documentation Makarius Wenzel 2022-12-02 20:29:40 +0100
  • 912d4bb49e Maintain document template in Isabelle/ML via Isar commands: result becomes export artifact, which is harvested by Isabelle/Scala build engine Makarius Wenzel 2022-12-02 20:05:15 +0100
  • a6c1a2baa4 Removed obsolete "extend" operation Makarius Wenzel 2022-12-02 15:31:23 +0100
  • bb5963c6e2 Proper usage of dof_mkroot, although its Bash pretty-printing in LaTeX is a bit odd Makarius Wenzel 2022-12-02 14:35:17 +0100
  • cc3e2a51a4 More antiquotations Makarius Wenzel 2022-12-02 13:50:16 +0100
  • 9e4e5b49eb More antiquotations from Isabelle2021-1/2022 Makarius Wenzel 2022-12-02 11:41:31 +0100
  • b65ecbdbef Updated to Isabelle2022 Makarius Wenzel 2022-12-02 10:34:15 +0100