Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity
1,362 Commits 15 Branches 10 Tags 77 MiB
Commit Graph

145 Commits

Author SHA1 Message Date
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
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 be0352cab7 ... 2022-01-26 09:24:20 +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 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
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
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
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 d2dcc71229 Removed explicit vspaces to clean up layout. 2021-01-04 06:32:56 +00:00
Burkhart Wolff aee1d33709 renaming ISA's; new shortcuts; more content in the RefMan. 2021-01-02 15:57:28 +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 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 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
Achim D. Brucker 538292b972 Fixed LaTeX compiliation error. 2020-10-06 04:45:30 +01:00
Burkhart Wolff bea648530b pushup. 2020-09-22 16:57:50 +02:00
Burkhart Wolff 9956bbf062 pushup, stiluebungen. 2020-09-22 16:35:28 +02:00
Burkhart Wolff 2d2f4320e0 intermediate status with LaTeX pblsm 2020-09-09 13:17:22 +02:00
Achim D. Brucker ee251a8000 Removed unused LaTeX definitions and style files. 2020-09-08 00:01:50 +01:00
Achim D. Brucker 7956a3009a Initial commit: style for providing theorem-like default environments. 2020-09-07 23:56:43 +01:00
Achim D. Brucker 75719a933a Added 2020-iFM-CSP example based on scrartcl.cls. 2020-09-07 23:35:43 +01:00
Burkhart Wolff 2321945dc4 sdf 2020-09-07 23:17:36 +01:00
Burkhart Wolff 7e2224859e mmm 2020-06-22 17:42:40 +02:00
Burkhart Wolff 0c4a5a5fea eliminating deprecated syntax 2020-04-09 23:58:58 +02:00
Achim D. Brucker 60ebbbe12c Updated license information.
Isabelle_DOF/Isabelle_DOF/master This commit looks good Details
2019-08-15 15:09:55 +01:00
Achim D. Brucker 6cd8cb098b Updated license information.
Isabelle_DOF/Isabelle_DOF/master This commit looks good Details
2019-08-15 14:52:15 +01:00
Achim D. Brucker b1d4abbf48 Introduced \dofurl.
Isabelle_DOF/Isabelle_DOF/master This commit looks good Details
2019-08-12 08:28:16 +01:00
Achim D. Brucker 6e6c4a81cb Updated Isabelle/DOF repository URL.
Isabelle_DOF/Isabelle_DOF/master This commit looks good Details
2019-08-04 22:47:52 +01:00
Achim D. Brucker 9c7f6f6a28 Renamed DOF_mkroot to mkroot_DOF.
Isabelle_DOF/Isabelle_DOF/master This commit looks good Details
2019-08-03 21:36:06 +01:00
Achim D. Brucker 94fdf75627 Applied renaming: Paris-Sud to Paris-Saclay.
Isabelle_DOF/Isabelle_DOF/master This commit looks good Details
2019-07-28 12:01:58 +01:00
Achim D. Brucker 36f7ebc4bf Fixed naming inconsistency. 2019-07-23 07:41:27 +01:00
Achim D. Brucker eef387198a Updated URL of Isabelle/DOF repository. 2019-07-21 10:22:06 +01:00
Achim D. Brucker d1f55e7f30 Do not include checking instructions in PDF. 2019-07-21 10:21:37 +01:00
Achim D. Brucker 6fd22a071f Resolved naming inconsistency (mathex_onto vs. math_exam).
Isabelle_DOF/Isabelle_DOF/master There was a failure building this commit Details
2019-07-20 21:51:55 +01:00
Achim D. Brucker 8953f37629 Large directory restructuring.
Isabelle_DOF/Isabelle_DOF/master This commit looks good Details 
This commit restructures the file hierarchy:
1) implementation is moved into src/ directory to clean up
   the main directory and to make it easier for users to
   find the README.md.
2) ontologies (both, the Isabelle-part and the LaTeX-part) are
   now structured into directories.
 2019-07-20 21:12:40 +01:00
Burkhart Wolff 3b4e82b27c New autoref - format, ...
HOL-OCL/Isabelle_DOF/Isabelle2018 There was a failure building this commit Details
HOL-OCL/Isabelle_DOF/Isabelle2019 There was a failure building this commit Details
Isabelle_DOF/Isabelle_DOF/Isabelle2019 There was a failure building this commit Details
2019-05-28 10:43:40 +02:00
Achim D. Brucker 773b20b918 Cleanup. 2019-01-08 15:54:38 +00:00
Achim D. Brucker db866bc241 Merge branch 'master' of logicalhacking.com:HOL-OCL/Isabelle_DOF 2019-01-08 11:40:57 +00:00
Achim D. Brucker a0a6c47fc6 Changed project configuration to a single configuration file. 2019-01-08 11:06:33 +00:00
Burkhart Wolff 33602282a0 itp paper comments 
cenelec revision.
 2019-01-08 10:34:49 +01:00
Burkhart Wolff 9adfeb6425 Merge from Achim 
Merge branch 'master' of https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF
 2019-01-07 21:13:56 +01:00
Burkhart Wolff c443149647 First drafts on resubmission of the concept paper. 2019-01-07 21:13:23 +01:00
Burkhart Wolff dcd1a159c5 - deleted rubbish. 2019-01-07 21:12:01 +01:00
Achim D. Brucker 339c6733f2 Modularized build script to simplify automated updates. 2019-01-07 00:29:42 +00:00
Achim D. Brucker b91377edbd Base examples on the session Isabelle_DOF. 2019-01-06 18:22:54 +00:00
Achim D. Brucker d03052f4d6 Reworked root.tex setup. 
The root.tex is now copied from the user installation directory
on each build to avoid problems with an outdated document setup.
 2019-01-06 17:01:13 +00:00
Achim D. Brucker 5f5e8694d1 Updated root.tex files. 2019-01-06 14:38:05 +00:00
Achim D. Brucker 75ff2fad2d Revert "Removed obsolete build scripts." 
This reverts commit 30a17db2bf.
 2019-01-06 13:34:58 +00:00
Achim D. Brucker 30a17db2bf Removed obsolete build scripts. 2019-01-05 23:38:56 +00:00
Achim D. Brucker e0c5c81e1d Made upqoute and beramono optional. 2018-12-19 16:05:27 +00:00
Achim D. Brucker 87ee897983 Disabled upqoute - not part of texlive 2017. 2018-12-19 15:55:29 +00:00
Burkhart Wolff eae495ac90 - Added monitor class-invariant for level consistency. 
- debugging here and there
- integration test
- remark : MathExam is in a pretty inconsistent state (requires discussion)
- integration test
 2018-12-18 14:29:08 +01:00
Burkhart Wolff 98565b837c Worked on assert*. 
Still needs debugging.
Regression tests of some examples;
necessary revisions due to stronger
checks at close_monitor.
 2018-12-11 16:03:01 +01:00
Burkhart Wolff 5e7ac1c02e - Fixed the FrontEnd - level problem according to what we discussed: 
-- there are classes that do not have a level
-- title, subtitle and abstract DO NOT HAVE a level
-- text* has a level, but the level "None"

- Tested whatever we have as examples
 2018-12-04 10:41:34 +01:00
Achim D. Brucker 1f2551d683 Restrucuring. 2018-11-27 13:39:54 +00:00
Achim D. Brucker 21d51e7275 Restrucuring. 2018-11-27 13:22:31 +00:00
Achim D. Brucker 9d5bddea7c Restrucuring. 2018-11-27 13:11:54 +00:00