| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2024-06-12 | Prove Bug "Ex falso quodlibet" | Simon-Kor | |
| The generated ATP Tasks are done in few secounds, if they are send manually to Vampire. But if its done in Naproche all together it won't work. | |||
| 2024-06-11 | proof of complement_interior_eq_closure_complement and some more about ↵ | Simon-Kor | |
| clousures(unsatable) | |||
| 2024-06-10 | Dedupe helper function | adelon | |
| 2024-06-05 | Update Megalodon.hs | adelon | |
| 2024-06-04 | Proof of teetwo_space_is_teeone_space | Simon-Kor | |
| 2024-06-04 | Proof of teeone_implies_singletons_closed | Simon-Kor | |
| The Assumption was changed, for usage of bounded variables. Maybe there is a bug with Omitted. Omitted restricts the Ambigus Phrase testing. | |||
| 2024-06-04 | Some notation fixes and lemma for topo basis generats opens was proofed and ↵ | Simon-Kor | |
| optimizised | |||
| 2024-05-28 | Merge pull request #2 from adelon/main | Simon-Kor | |
| changes from main needs to be included | |||
| 2024-05-28 | Merge branch 'main' into main | Simon-Kor | |
| 2024-05-28 | unexpected behavior of vampire | Simon-Kor | |
| The task topological behavior is proofed in seconds by just vampire, but with mode casc it takes plenty seconds | |||
| 2024-05-28 | Update `inters_in_genopens` | adelon | |
| 2024-05-28 | Pow closed under binary intersection | adelon | |
| 2024-05-28 | Merge branch 'main' into main | Simon-Kor | |
| 2024-05-28 | proofing some lammes about topological basis | Simon-Kor | |
| 2024-05-25 | Prove `emptyset_open` to replace structure axiom | adelon | |
| 2024-05-23 | Update formatting | adelon | |
| 2024-05-22 | Update filter.tex | adelon | |
| 2024-05-22 | Add filter lemmas | adelon | |
| 2024-05-22 | Add lemma `filter_setminus_in` | adelon | |
| 2024-05-22 | Update label for `genopens` | adelon | |
| 2024-05-22 | Update defaulting for envvar | adelon | |
| 2024-05-22 | Allow `\left` and `\right` everywhere | adelon | |
| 2024-05-21 | Allow line breaks via `\textbox`, handle `\left`/`\right` | adelon | |
| 2024-05-21 | Add definition for `\genOpens` | adelon | |
| 2024-05-21 | Add simple lemmas on filters | adelon | |
| 2024-05-16 | Attach whitespace info to located token | adelon | |
| 2024-05-16 | Fix missing `\text` | adelon | |
| 2024-05-14 | Merge branch 'adelon:main' into main | Simon-Kor | |
| 2024-05-14 | work on metric spaces | Simon-Kor | |
| 2024-05-14 | Update Api.hs | adelon | |
| 2024-05-14 | Update basis.tex | adelon | |
| 2024-05-07 | Merge branch 'adelon:main' into main | Simon-Kor | |
| 2024-05-07 | Update noun guessing | adelon | |
| 2024-05-07 | Merge branch 'adelon:main' into main | Simon-Kor | |
| 2024-05-07 | formalisation mertic optimized | Simon-Kor | |
| 2024-05-07 | Sketch noun coord, symbols for reals | adelon | |
| 2024-05-07 | Sketch lexicon mechanism | adelon | |
| 2024-05-07 | Clean up of Notation in numbers.tex | Simon-Kor | |
| First notation of tupels in the relation set was swapped with the canonical <. | |||
| 2024-05-07 | Formalization of metric spaces and some cleaning of numbers.tex | Simon-Kor | |
| Formalization of metric spaces: Therefore we introduced the predicate metric and its axiomatization. Then we introduced the term metric space in dependence of a metric function. This metric space is automatically a a topological space. | |||
| 2024-04-30 | Merge branch 'adelon:main' into main | Simon-Kor | |
| 2024-04-30 | Adding the first formalisation of reals | Simon-Kor | |
| 2024-04-30 | Sketch new signature syntax | adelon | |
| 2024-04-13 | first formalisation of addition on naturals | Simon-Kor | |
| We try to Implement the Addition on natural numbers by a relation on N \times N to N such that some of the axioms of the addition holds | |||
| 2024-04-11 | Set the Headline Order for the corresponding section | Simon-Kor | |
| 2024-04-11 | Merge pull request #1 from adelon/main | Simon-Kor | |
| Update Fork | |||
| 2024-04-11 | Formalisation of groups and monoids | Simon-Kor | |
| The test.tex file was deleted and all formalisations of groups and monoids was moved to the fitting document of the library. Some proof steps of the new formalisation were optimized for proof time | |||
| 2024-04-01 | Allow numbers in markers (from the second char) | adelon | |
| 2024-03-31 | Report_in_text_file | Simon-Kor | |
| Txt File Error.txt has been filled | |||
| 2024-03-31 | Possible_Bug | Simon-Kor | |
| In File test.tex line 51 could not be proven, error massage is in the new file error.txt | |||
| 2024-03-28 | Merge pull request #1 from Simon-Kor/main | adelon | |
| Allow Windows-style newlines | |||
 |
index : naproche-zf.git | |
| Unnamed repository; edit this file 'description' to name the repository. |
| summaryrefslogtreecommitdiff |