pierre.derathe
/
Isabelle_DOF
Archived
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
1,515 Commits 15 Branches 8 Tags 73 MiB
Commit Graph

748 Commits

Author SHA1 Message Date
Idir AIT SADOUNE f674ca8ca3 updating Idir's part and papser structure 2022-02-08 09:47:47 +01:00
Idir AIT SADOUNE 7cd7a4d15d updating Idir's part 2022-02-08 09:40:41 +01:00
Idir AIT SADOUNE b9c72124c0 Updating Idir's part in the paper 2022-02-08 09:21:50 +01:00
Burkhart Wolff fe728ef9af polishing 2022-02-08 07:14:11 +01:00
Burkhart Wolff c2fa80953a Draft of Conclusion 2022-02-08 06:56:28 +01:00
Burkhart Wolff f180a87fbf merge 2022-02-07 23:58:36 +01:00
Burkhart Wolff 3226fdf0c8 added elements in Conclusion Related Work 2022-02-07 23:56:35 +01:00
Idir AIT SADOUNE f35a7eb5bd Adding Idir's part to the paper 2022-02-07 21:28:40 +01:00
Nicolas Méric 34a57b2c9f Update typo 2022-02-07 20:09:10 +01:00
Burkhart Wolff 17c6e87b8d updated Idirs example 2022-02-07 18:59:14 +01:00
Nicolas Méric 9d3b701c27 Update authors in preamble 2022-02-07 15:24:31 +01:00
Nicolas Méric 46450e951c Add orcid logo 2022-02-07 14:51:55 +01:00
Nicolas Méric 307bb4e3d4 Add lipics and cc logos 2022-02-07 14:43:02 +01:00
Nicolas Méric 1051e2cd7b Update invariants section 2022-02-07 10:32:05 +01:00
Nicolas Méric c914b201ee Update invariants section 2022-02-07 09:52:56 +01:00
Nicolas Méric b2aac7288d Add OntoMathPro section and update invariants section 2022-02-06 20:34:39 +01:00
Nicolas Méric 94baf69f25 Update invariants section 2022-02-04 17:41:43 +01:00
Nicolas Méric 68417e01d3 Update invariants-section 2022-02-04 15:10:46 +01:00
Nicolas Méric 30793f5c51 Update invariants section 2022-02-04 15:08:47 +01:00
Nicolas Méric 09129bfbf8 Update titlerunning and clean up text 2022-02-03 15:19:09 +01:00
Nicolas Méric 2e645ed5ff Update structure of Advanced Evaluation section 2022-02-03 11:33:56 +01:00
Burkhart Wolff 092d552ef8 fixed bugs 2022-02-03 11:30:22 +01:00
Nicolas Méric 927f0446a0 Update invariants section 2022-02-03 11:04:39 +01:00
Nicolas Méric 7033335e3f Update extensible record section 
Update text to reflect that a property apply on the scheme type
of the record
 2022-02-03 09:06:10 +01:00
Nicolas Méric a2f3057545 Update extensible record section 
Make it compile
 2022-02-03 09:00:53 +01:00
Burkhart Wolff e6721b548d added 2 sections in background. 2022-02-02 23:04:37 +01:00
Burkhart Wolff d319ab2555 section on extensible records 2022-02-02 17:03:17 +01:00
Nicolas Méric 502f5c5cd2 Switch to lipics template and update invariants section 2022-02-02 12:43:51 +01:00
Nicolas Méric 7ac669e52e Update invariants section 2022-01-31 17:38:37 +01:00
Nicolas Méric d9f2d5c0c4 Merge branch 'master' into 2021-ITP-PMTI 2022-01-31 13:09:26 +01:00
Nicolas Méric 8f7e898f4b Fix invariant railroad diagram 2022-01-31 13:01:59 +01:00
Burkhart Wolff 9d9fd03b72 minor stuff 2022-01-30 20:59:21 +01:00
Burkhart Wolff 05b896291b ... 2022-01-30 14:56:22 +01:00
Burkhart Wolff cc151291f6 some figures on MathTaxonomies 2022-01-30 14:55:19 +01:00
Burkhart Wolff 3e06e659b6 global restructuring 2022-01-30 14:50:22 +01:00
Burkhart Wolff b35c774d27 polished intro 2022-01-30 13:47:18 +01:00
Burkhart Wolff c5cdf5f826 revised introduction 2022-01-29 22:27:30 +01:00
Nicolas Méric a38d13198c Add invariants and queries draft in 2021-ITP-PMTI 2022-01-28 17:18:09 +01:00
Burkhart Wolff 9cd021d7fa new paper structure 2022-01-26 11:53:00 +01:00
Burkhart Wolff b1fb509d8b Modifs of title and abstract 2022-01-26 11:16:32 +01:00
Burkhart Wolff 63145e0d3a Merge branch '2021-ITP-PMTI' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF into 2021-ITP-PMTI 2022-01-26 09:24:29 +01:00
Burkhart Wolff be0352cab7 ... 2022-01-26 09:24:20 +01:00
Nicolas Méric 6d42f122b1 Merge branch 'master' into 2021-ITP-PMTI 2022-01-25 08:52:52 +01:00
Nicolas Méric 76612ae6f3 Add checking of invariants for class instances 
- Warning: the current implementation does yet not support
    some use-cases, like invariant on monitors,
    or the initialization of docitem without a class associated.
- Add first draft of the checking of invariants.
  For now, it is disabled by default because some cases
  are not yet supported, like the initialization of docitem
  without a class associated.
  ex: text*[sdf]‹ Lorem ipsum @{thm refl}›
- To enable the checking, one can use the theory attribute
  "invariants_checking" by declaring it in a theory like this:
  declare [[invariants_strict_checking = true]]
- A checking using basic tactics (unfolding and auto) can be enable
  with the "invariants_checking_with_tactics" theory attribute
  for specific use-cases
- The specification of invariants is now automatically abstracted,
  so one must define an invariant like this now:

  doc_class W =
  w::"int"
  invariant w :: "w σ ≥ 3"

  The old form:

  doc_class W =
  w::"int"
  invariant w :: "λσ. w σ ≥ 3"

  is now deprecated.
  The specification of the invariant still uses the σ-notation
  and is defined globally by the name component "invariantN"
- Update the invariants definition in the theories to match
  the new implementation
- Update the manual to explain this new feature
- Add small examples in src/tests/High_Level_Syntax_Invariants.thy
  and src/tests/Ontology_Matching_Example.thy
 2022-01-24 17:30:48 +01:00
Burkhart Wolff e53984feea Merge branch '2021-ITP-PMTI' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF into 2021-ITP-PMTI 2022-01-20 22:08:38 +01:00
Burkhart Wolff d7c7a98138 added elements to related work: OntoMathPro, ScienceWISE, DBpedia 2022-01-20 22:08:32 +01:00
Idir AIT SADOUNE 8629dda85e first version of a case study 2022-01-20 10:59:17 +01:00
Nicolas Méric 688e823463 Make 2021-ITP-PMTI paper compile 2022-01-19 09:40:05 +01:00
Burkhart Wolff 96112ff893 restored ancient SEFM paper example for invariants 2022-01-17 12:06:32 +01:00
Burkhart Wolff 5631010371 added figures from IFM 19 paper 2022-01-14 15:31:15 +01:00
Burkhart Wolff 68e9f64156 added figures from talk 2022-01-13 16:24:07 +01:00
Burkhart Wolff 647f8e86cc Reorg / shoprtening chap 2. 2022-01-11 20:53:07 +01:00
Burkhart Wolff b5939bc9db added basckground chapter . First flush. 2022-01-08 22:22:22 +01:00
Burkhart Wolff 6889e08f33 initial setup of RAS paper 2022-01-02 17:05:15 +01:00
Burkhart Wolff ef7d8caefb added background chapter 2022-01-01 21:03:31 +01:00
Makarius Wenzel 4e4995bde5 Isabelle/Scala build.props with some pro-forma services 
(unusual package name prevents problems with Maven/IntelliJ).
 2021-12-19 16:50:21 +01:00
Burkhart Wolff 96d6bb8e00 intro proposal completed 2021-12-19 13:31:42 +01:00
Burkhart Wolff 77150aefe2 more on intro 2021-12-19 10:38:00 +01:00
Makarius Wenzel 86b555b56e Disable TR_my_commented_isabelle for now: does not work with Isabelle2021-1. 2021-12-18 23:07:25 +01:00
Makarius Wenzel ec49f45966 Adaptations for Isabelle2021-1. 2021-12-18 23:06:51 +01:00
Burkhart Wolff 12d33fa457 more on intro ... 2021-12-17 15:44:47 +01:00
Burkhart Wolff 616ff85721 ... 2021-12-16 15:13:34 +01:00
Burkhart Wolff b0a2214c40 added refs 2021-12-16 15:07:02 +01:00
Burkhart Wolff cbd32874cf Abstract 2021-12-16 14:55:04 +01:00
Burkhart Wolff 3f09aca090 added paper frame, small things. 2021-12-16 13:49:44 +01:00
Burkhart Wolff 9b08e92588 Experiments with the code generator for Isa_DOF class objects. 2021-10-08 16:00:57 +02:00
Burkhart Wolff 5f47588270 added some value-statements for demonstration purposes 2021-10-05 16:22:05 +02:00
Burkhart Wolff eb292a695b added poor man's encoding of inheritance in Cyto-Model. 2021-10-04 15:11:29 +02:00
Burkhart Wolff 3f8880c0f0 added small fun ontology for examples : Cytology 2021-09-29 14:08:28 +02:00
Nicolas Méric f11e5b762b all changes 2021-06-01 14:51:22 +02:00
Burkhart Wolff f8801a1121 basically table_inline. 2021-05-13 14:37:27 +02:00
Achim D. Brucker 920779b150 Raised requirement of Tex Live to TeX Live 2021 (expected release date: 4th of April 2021). 2021-03-22 00:13:18 +00:00
Achim D. Brucker 712cea7ac9 Merge branch 'v1.1.x/Isabelle2020' 2021-03-20 22:26:14 +00:00
Achim D. Brucker a0654d8db9 Added Nicolas Méric as contributor. 2021-03-20 22:05:57 +00:00
Achim D. Brucker e048bbe508 Merge branch 'master' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF 2021-03-15 10:25:16 +00:00
Achim D. Brucker 201d12a01a Fixed spelling. 2021-03-15 10:24:58 +00:00
Burkhart Wolff cfad21e296 Ref auf Makarius Text added 2021-03-14 15:45:42 +01:00
Achim D. Brucker 389fd6d033 Switch from pdf(la)tex to lua(la)tex. 2021-03-10 23:51:18 +00:00
Achim D. Brucker f975672901 Removed check for \expanded{}: Isabelle 2021 defaults to luatex as TeX-engine, which has \expanded{} since a very long time. 2021-03-10 22:12:39 +00:00
Achim D. Brucker 06dddeacf5 Porting to Isabelle 2021. 2021-03-10 22:04:09 +00:00
Achim D. Brucker e495a7b2fe Revising Chapter 5. 2021-02-13 17:04:17 +00:00
Achim D. Brucker 018bfa4bcd Added default escapechar for ltx environment. 2021-02-12 02:24:31 +00:00
Achim D. Brucker 15c958ec64 Revised Chapter 4. 2021-02-11 19:10:38 +00:00
Achim D. Brucker 29661f6734 Revised Sec. 4.2. 2021-02-10 09:05:59 +00:00
Achim D. Brucker 3649fb855e Revised Sec. 4.1. 2021-02-09 20:56:56 +00:00
Achim D. Brucker 43184a9995 Migrated \inlinebawsh{}. 2021-02-08 15:34:59 +00:00
Achim D. Brucker ed8cd2ad9d Migrated \inlinebawsh{}. 2021-02-08 15:33:45 +00:00
Achim D. Brucker 029ae709e6 Migrated \inlineltx{}, except when argument contained { or }. 2021-02-07 20:01:43 +00:00
Achim D. Brucker 85d94848b6 Revised Chapter 3. 2021-02-06 12:08:18 +00:00
Achim D. Brucker b61346fd64 Revised Sec. 3.2. 2021-02-05 06:58:22 +00:00
Achim D. Brucker 3d0cbf6a4f Revised Sec. 3.1. 2021-02-04 18:52:38 +00:00
Achim D. Brucker 50d3dde1a0 Converted \inlinesml{...}. 2021-02-03 05:13:05 +00:00
Achim D. Brucker d605e23218 Converted \inlinesml{...}. 2021-02-02 12:22:35 +00:00
Achim D. Brucker 2d3e521296 Converted \inlinebash{...}. 2021-02-02 12:20:03 +00:00
Achim D. Brucker b81eef7bd2 Converted bash-environments to antiqotations. 2021-02-01 05:06:15 +00:00
Achim D. Brucker a1332ec9a4 Converted bash-environments to antiqotations. 2021-01-31 16:54:22 +00:00
Achim D. Brucker 243556467a Merge remote-tracking branch 'origin/add-todos-fix-typos' 2021-01-30 06:47:47 +00:00
Nicolas Méric 4d9de40037 Add TODOs to improve the wording 2021-01-28 13:04:29 +01:00
Nicolas Méric 76266fbd5e Add TODOs to improve text consistency 
There are some inconsistencies between some figures and the text
which refers to them.
 2021-01-28 12:59:48 +01:00
Nicolas Méric 1fb97c8fb0 Add TODOs to delete references to where clause 
The where clause for ontology classes is deprecated
in favor of the accepts and rejects clauses.
 2021-01-28 12:48:54 +01:00
Nicolas Méric 5b618562a2 Fix some typos 2021-01-28 12:46:20 +01:00
Achim D. Brucker e9fc175cb6 Cleanup. 2021-01-25 23:34:23 +00:00
Achim D. Brucker 7e3c82f65e Cleanup. 2021-01-21 16:20:27 +00:00
Achim D. Brucker b4482b02d9 Modernized comment syntax. 2021-01-20 23:25:17 +00:00
Achim D. Brucker a9737762fd Fixed spacing in front of index entries.. 2021-01-19 23:12:58 +00:00
Achim D. Brucker fc2817db0d Cleanup. 2021-01-18 20:30:39 +00:00
Achim D. Brucker 6ed771ef04 Workaround to support lualatex. 2021-01-17 06:37:14 +00:00
Achim D. Brucker 9e605d2e3c Removed fixme. 2021-01-15 00:46:29 +00:00
Achim D. Brucker 6927781d26 Merge. 2021-01-09 06:32:17 +00:00
Achim D. Brucker 7e01ff7021 Cleanup. 2021-01-08 03:54:37 +00:00
Achim D. Brucker 82121d7204 Cleanup. 2021-01-07 04:39:28 +00:00
Achim D. Brucker 225309482b Updated copyright information. 2021-01-06 06:48:36 +00:00
Achim D. Brucker 78a17a66b5 Fixed copyright header. 2021-01-05 11:32:26 +00:00
Achim D. Brucker 20b3e7c0b7 Removed pdflatex check (TeX Live 2019 should available everywhere and the dependency is still checked during installation. 2021-01-05 11:25:55 +00:00
Achim D. Brucker d2dcc71229 Removed explicit vspaces to clean up layout. 2021-01-04 06:32:56 +00:00
Burkhart Wolff d86e708154 a first imprfect solution for the assert* problem; 4th chapter roughly completed. 2021-01-03 14:07:21 +01:00
Burkhart Wolff aee1d33709 renaming ISA's; new shortcuts; more content in the RefMan. 2021-01-02 15:57:28 +01:00
Burkhart Wolff b71be9c4a8 Reorganization Chap 4. <4.3.2 2021-01-01 21:34:05 +01:00
Burkhart Wolff 396ef1d477 More content in 4, better tree printing. 2021-01-01 21:23:21 +01:00
Burkhart Wolff 950a86aa5a Adding better explanation of the core functionalities... 2021-01-01 16:12:07 +01:00
Burkhart Wolff 480f0ada37 Reorganization Chap 4. ... 2020-12-31 11:02:27 +01:00
Burkhart Wolff 242bb536bc Reorganization Chap 4. <4.3.2 2020-12-30 23:07:19 +01:00
Burkhart Wolff d6832cc8f8 Reorganization Chap 4. 2020-12-30 15:06:11 +01:00
Burkhart Wolff 04f0cc7f5c Reorganization: Pushed Macro Core Mechanism into the DOF Core; adapted the RefMan accordingly. 2020-12-30 12:47:54 +01:00
Burkhart Wolff 2f721d0f4b activated syntactic checks for trimming macros 2020-12-24 04:53:27 +01:00
Burkhart Wolff 4c5aacb39f activated syntactic checks for trimming macros 2020-12-23 11:30:42 +01:00
Burkhart Wolff 005922ffda built in syntactic checks for trimming macros 2020-12-23 09:41:26 +01:00
Burkhart Wolff 6899c4059e improved macro syntax 2020-12-22 20:37:15 +01:00
Burkhart Wolff 5593c22a36 first version with macro syntax (no ML support) 2020-12-22 19:50:00 +01:00
Burkhart Wolff de5c0fc6e2 added Isar-syntax for define_shortcut* 2020-12-22 08:07:19 +01:00
Burkhart Wolff 0e64608a58 enforcing shorter Definition* - style in examples (CC,CENELEC,...) 2020-12-02 09:32:48 +01:00
Burkhart Wolff 8771d8581b default class checking bug fixed; new attributes for default classes in ontological macros Definition* Theorem* Lemma* 2020-12-01 23:18:13 +01:00
Burkhart Wolff 698da3dd24 intermediate session with Macro-Bug. 2020-11-24 10:57:17 +01:00
Burkhart Wolff efeee1e863 Eliminated deprecated abstract class residuals; lifted Definition* to math_content. 2020-11-10 13:07:54 +01:00
Burkhart Wolff 2ecb62a80e added Lemma*, Theorem* and Definition* support. Bug: referencing does not work. 2020-11-04 15:55:43 +01:00
Burkhart Wolff da0f3e63f1 more steps to reform document macro mechanism 2020-11-04 13:13:24 +01:00
Burkhart Wolff 7f4b587274 steps to reform cicm/csp paper and manual 2020-11-04 11:18:43 +01:00
Burkhart Wolff dc7ed74c57 Second steps to reform cicm paper 2020-11-04 10:12:31 +01:00
Burkhart Wolff 84c7cabec0 First steps to reform cicm paper 2020-11-04 09:22:49 +01:00
Burkhart Wolff fbefa85586 First steps to reform cicm paper 2020-11-04 03:27:24 +01:00
Burkhart Wolff c991e693dc tested and enforced new author* and abstract* macros. 2020-11-04 02:52:55 +01:00
Achim D. Brucker 0b52e5872d Use author*. 2020-11-03 21:50:19 +00:00
Burkhart Wolff bad7dfc2ef new set of macros : author* and abstract* --- not working yet 2020-11-03 19:00:33 +01:00
Burkhart Wolff fe8f63690d macro-arrangement ... 2020-11-02 18:30:40 +01:00
Burkhart Wolff 1f403a09f6 dfg 2020-11-02 14:14:52 +01:00
Burkhart Wolff abd32a802d First Pass of Chap 4 - Added invariant syntax description, more semantic content 2020-10-26 12:27:33 +01:00
Burkhart Wolff f093b033f5 started pass on chap 4 in Refman. 2020-10-26 10:08:22 +01:00
Burkhart Wolff 3ba9454ac7 Slight improvements of the layout 2020-10-25 12:57:43 +01:00
Burkhart Wolff 3c6197e6ca FINISHED MY PASS ON THE PROGRAMMING MANUAL. 2020-10-25 12:02:44 +01:00
Burkhart Wolff 7999ee9a38 recvision till line 2000 (Term Parsing) 2020-10-21 13:49:01 +02:00