Changes

Summary

1. Some hyphens that should be en dashes
2. slightly refine WPO-definition - previous formalization of WPO deviated a bit to paper version (requiring less computation) - both versions are equivalent whenever order in parameter is strongly normalizing - however, this is no longer true for co-WPO, a variant of WPO with non strongly normalizing orders - consequence: change formalization so that it is more closely related to paper version, so that also results on coWPO can be proven
3. merged
4. no "open" of ML structures: it makes sources unmaintainable;
5. adapted to Isabelle/5db014c36f42;
6. adapted to Isabelle/f4cd6e3b5075;
7. adapted to Isabelle/5db014c36f42;
8. This file should have been removed in the previous commit.
9. Sync with my development repo. Main changes related to CartesianMonoidalCategory.
10. update timing;
11. eliminated pointless parallelism: approx. 1.3s as plain sequential ML;
12. tuned;
13. alternative version by Manuel Eberl, following the approach of Isabelle2022/src/HOL/Tools/sat.ML with one big hyp;
14. adapted to Isabelle/c274f52b11ff;
15. Backed out changeset a537fb4c92af
16. slightly faster thanks to Thm.shared_context from Isabelle/4f9117e6020d;
17. merged
18. moved lemma to FDS exercises
19. Fix proofs broken by previous commit.
20. Add congurence rule for bind_tm in Root_Balanced_Tree.Time_Monad The rule is necessary for the termination proof of some recursive functions over the time monad.
21. tuned;
22. tuned;
23. eliminated aliases: prefer existing Thm.elim_implies;
24. tuned;
25. more standard use of structure Unsynchronized;
26. tuned whitespace;
27. not unused!
28. Added running time analysis
29. some remarks on division
30. clarified scope of document
31. no subsection without section
32. merged
33. Deleted library material
34. adapted to Isabelle/b43ee37926a9;
35. merged
36. adapted to Isabelle/13cee8c2ed8d;
37. Add related entry for Combinatorial_Enumeration_Algorithms. Note: I followed APA style guide for the reference. https://apastyle.apa.org/style-grammar-guidelines/references/examples/published-dissertation-references Note: Ran sitegen.
38. small simplifications
39. shortened some parts of Huffman proof using Sledgehammer
40. added another simplification rule when alternatives are equal
41. added more simplification rules involving Zero
42. adapted to Isabelle/4a174bea55e2;
43. uodated map update syntax
44. Adjusted to changes in distribution.
45. more realistic timeout;
46. avoid hardwired documents; tuned whitespace;
47. merged
48. simplified a few proofs
49. added character sets to the extension directory of regular expressions
50. more syntax adjustments
51. more syntax update for map update syntax
52. more map update syntax updates
53. merged
54. updated to new map update syntax priorities
55. Some simplifications of proofs
56. Minor refinements
57. tiny simplifications
58. tidied another file
59. tidied a bit more
60. merged
61. More tidying
62. completed the addtion of Rec in the Extension directory
63. added another regular expression for Record
64. More tidying of the Ordinal entry
65. A massive tidying
66. Tiny bit more tidying
67. more robust: allow optional arguments in isabelle.Progress.echo;
68. More tidying
69. merged
70. Suppression of duplicate syntax for abs_summable_on, etc.
71. No more sorted_take, sorted_drop
72. Update entries MDP-Rewards and MDP-Algorithms
73. Migration of material from Jordan_Hoelder to HOL-Algebra
74. merged
75. Tidied up some messy proofs
76. Adjustments for the new infix status of has_sum
77. A tiny spelling correction
78. merged
79. A little more migration
80. Backed out changeset fa59c080cb3b
81. Backed out changeset 811f0b8d4f58
82. tuned metis call to avoid obscure feature
83. merged
84. Migration of material to the repository and necessary modifications
85. more map_of adaptions
86. adapted to new List.map_of
87. update Real_Time_Deque
88. Removal of a stray sledgehammer command
89. explicit range types in abstractions
90. somehow more clear terminology
91. merged
92. Some tidying and moving some material to the distribution
93. Deleted use of Euclidean_Division
94. Repaired session name
95. "Repaired boundary behaviour of mod+- for even modulus, Added locale module_spec for possible instantiation of Dilithium"
96. Update names to match thesis.
97. proper components base, following "isabelle components -I": downloaded components should be shared for all Isabelle versions;
98. proper symbolic handle on component resources (see Isabelle/3eb3de867786);
99. more realistic timeout, based on CPU time;
100. adapted to Isabelle/9a60c1759543;
101. more realistic timeout, based on CPU time;
102. fixed looping proofs
103. dropped reference to dead clone
104. removed dead clone
105. modernized
106. Modernized.
107. More instances.
108. Tuned whitespace.
109. Updated references.
110. More correct references.
111. Removed a bit of unnecessary material
112. merged
113. Shortened several messy proofs
114. Fix name clash in Frequency_Moments.
115. Fixed a name clash
116. Moving more material to the distribution
117. Moving some material to the main repository
118. adapted to db93f67a;
119. merged
120. generalized theory name: euclidean division denotes one particular division definition on integers
121. more efficient specification
122. merge from afp-2022
123. metadata for Suppes' theorem + sitegen
124. new entry: Suppes' Theorem
125. new entry HoareForDivergence
126. tuned css;
127. metadat for StrictOmegaCategories
128. new entry StrictOmegaCategories
129. tuned css;
130. cleanup accidental unused document files;
131. check ROOTs: add warning-only checks;
132. tuned;
133. add ROOT checks for document presence and unused files;
134. afp-submit visual improvements;
135. update bibtex example;
136. new doi
137. sitegen for AOT
138. merged
139. New entry AOT
140. New entry: Propositional_Logic_Class
141. sitegen for Cook_Levin
142. New entry Cook_Levin
143. Sorry — extra files for Boolos_Curious_Inference_Automated
144. Metadata for /Users/lp15/.isabelle/Isabelle2022/browser_info/AFP/Boolos_Curious_Inference_Automated
145. New entry Boolos_Curious_Inference_Automated
146. New entry: Synthetic_Completeness
147. New entry: Quantifier_Elimination_Hybrid
148. New entry Birkhoff_Finite_Distributive_Lattices
149. sitegen for Kneser_Cauchy_Davenport
150. metadata for Kneser_Cauchy_Davenport
151. new entry: Kneser_Cauchy_Davenport
152. sitegen for Turan
153. added metadata for Turans graph theorem
154. new entry: Turans Graph Theorem
155. new entry Multitape_To_Singletape_TM
156. removed static pages from rss feed;
157. Minor rerating of the abstract of Sauer_Shelah_Lemma
158. sitegen for /Users/lp15/.isabelle/Isabelle2022/browser_info/AFP/Sauer_Shelah_Lemma
159. New entry Sauer_Shelah_Lemma
160. sitegen for the aforementioned changes
161. adjustments to the abstract, requested by the author
162. CHERI-C_Memory_Model patch & metadata
163. New submission CHERI-C_Memory_Model
164. updated docs;
165. improve page layout slightly;
166. fixed broken abstract for PAPP_Impossibility
167. remove dead code
168. metadata and sitegen for PAPP_Impossibility
169. new entry PAPP_Impossibility
170. remove old .sitegen-ignore and mention AFP chapter in submission guidelines;
171. afp_check_roots: proper error message printing;
172. metadata and sitegen for Balog_Szemeredi_Gowers
173. new entry: Balog_Szemeredi_Gowers
174. tuned check names;
175. make check roots tool less dependent on AFP structure;
176. tuned;
177. web for Combinatorial_Enumeration_Algorithms
178. sitegen for Combinatorial_Enumeration_Algorithms
179. New entry Combinatorial_Enumeration_Algorithms
180. fix duplicate affiliations from author and notify;
181. add metadata check tool to sitegen;
182. update check tools: add formatting checks, new cmd options;
183. check for entries instead of session due to session nesting allowed in entries;
184. added unused thy check;
185. clarified check roots tool;
186. afp-submit: tuned logging;
187. afp-submit: encode new notify addresses properly;
188. afp-submit: correct build status on empty file;
189. afp-submit: remove padding on select;
190. re-format metadata;
191. afp-submit: update on correct status change;
192. afp-submit: clarified date format, tuned logging;
193. switch fonts to www prefixed isa-afp.org domain;
194. switch to www prefixed isa-afp.org domain;
195. clarified afp-submit error handling;
196. clarified afp-submit creation and message;
197. list submission system website;
198. afp-submit: clarified api urls;
199. Removal of more unused material
200. Small simplifications. Removed a needless assumption.
201. isabelle update -u cite;
202. more accurate root.bib, based on original \bibitem entries in root.tex 1a42ddd5dbbc;
203. Fixed the bib issues and supplied a root.bib based on the one in Types_Tableaus_and_Goedels_God (by the same author)
204. merged
205. Added the missing .bib file
206. proper bib context for formal citations, although there is no document;
207. back to unchecked \cite: entry lacks .bib file;
208. back to unchecked \cite: entry lacks .bib file;
209. back to unchecked \cite: there is entry lacks .bib file;
210. proper citation;
211. merged
212. added lemmas image_grounding_of_cls_grounding_of_cls and grounding_of_clss_grounding_of_clss[simp]
213. merged
214. isabelle update -u cite;
215. merged
216. consistent casing in \cite
217. ETTS: updated bibliography and citations
218. merged
219. more correct and complete citations;
220. unchecked \cite for unidentifiable citation;
221. proper @{cite} syntax;
222. isabelle update -u cite;
223. Updating Risk Free Lending Entry - Adding lemma for transfers in special case - Fixing grammar in abstract - Adding citation
224. added bibliography to ROOT;
225. CTR and ETTS: several amendments (fact names, printing, presentation)
226. Removed a reference to the (redundant) wf_restr
227. added bibliographies to ROOTs;
228. Changes for generalised lemmas
229. Changes for generalised lemmas
230. Generalised Lemmas
231. merged
232. adapted to Isabelle/c9e091867206
233. tuned;
234. tuned signature, following Isabelle/947510ce4e36;
235. adapted to Isabelle/25900fbea7ad; fewer clones of Isabelle sources;
236. adapted to Isabelle/b61ad889dffa
237. removed Restricted_Predicates.transp_on following the introduction of equivalent Relation.transp_on in HOL
238. merged
239. adapted to Isabelle/d33fc5228aae
240. fixed proof following Isabelle/66cae055ac7b
241. merge
242. adapted to Isabelle/c48fe2be847f
243. enable -no-pie for CakeML
244. fixed proofs and removed duplicates following Isabelle/e65a50f6c2de
245. tuned proofs to use asymI, asymD, asympI, and asympD
246. Fix failing continuous integration
247. fixed proof following Isabelle/8fff4e4d81cb
248. removed Restricted_Predicates.antisymp_on following the introduction of equivalent Relation.antisymp_on in HOL
249. added lemma imgu_range_vars_subset
250. Update headers and metadata.
251. Fix ROOT again
252. Fix ROOT
253. Use transfinite induction to prove Lindenbaum's lemma, removing the countable assumption.
254. Fixed proofs following Isabelle/a7d2a7a737b8
255. added lemmas mem_range_varsI and imgu_subst_domain_subset
256. weakened the definition of redundant_inference
257. removed Restricted_Predicates.irreflp_on following the introduction of equivalent Relation.irreflp_on in HOL
258. fixed Containers following introduction of irrefl_on
259. added lemmas ex_unify_if_unifiers_not_empty, ex_mgu_if_unifiers_not_empty, and imgu_range_vars_of_equations_vars_subset
260. name change
261. AFP and DBLP
262. merged
263. added lemmas subst_range_rename_subst_domain_subset and range_vars_rename_subst_domain_subset
264. added lemma subst_domain_rename_subst_domain_subset
265. added lemma image_the_Var_image_subst_renaming_eq
266. Added acknowledgements
267. Added code export to ROOT
268. Removed out of place code
269. tuned lemma subst_domain_restrict_subst_domain
270. added lemmas rename_subst_domain_range_Var_lhs[simp] and rename_subst_domain_range_Var_rhs[simp]
271. added attribute [simp] to lemma rename_subst_domain_Var_rhs
272. added lemmas inj_on_Var[simp] and rename_subst_domain_Var_lhs[simp]
273. merged
274. removed Restricted_Predicates.reflp_on following the introduction of equivalent Relation.reflp_on in HOL
275. removed Restricted_Predicates.total_on following the introduction of equivalent Relation.totalp_on in HOL
276. added lemmas grounding_of_subst_cls_renaming_ident[simp] and grounding_of_subst_clss_renaming_ident[simp]
277. added lemmas is_ground_cls_add_mset[simp], grounding_of_subst_cls_subset, and grounding_of_subst_clss_subset
278. Streamlined a proof
279. added lemmas
280. moved lemma around
281. redefined mgu as a definition
282. tuned naming
283. fixed proof
284. added definition restrict_subst_domain and associated lemmas
285. tuned (sub)subsection
286. added lemma member_image_the_Var_image_subst
287. added lemmas unify_subst_domain_range_vars_disjoint
288. added lemma unify_range_vars
289. added lemma unify_subst_domain
290. added definition rename_subst_domain_range and related lemmas
291. merged
292. added lemmas vars_term_subst_apply_term and vars_term_subst_apply_term_subset
293. Fixed the ROOT file, so that the theory of cardinals is loaded
294. added lemma ex_mgu_if_subst_apply_term_eq_subst_apply_term
295. added lemmas unify_append_prefix_same, unify_Cons_same, unify_same, and mgu_same
296. added lemma decompose_same_Fun[simp]
297. added lemma zip_option_same[simp]
298. added definition rename_subst_domain and lemma renaming_cancels_rename_subst_domain
299. removed simp annotation from subst_apply_term_eq_subst_apply_term_if_mgu
300. used rho for renamming
301. tuned assumptions
302. added lemma subst_apply_term_eq_subst_apply_term_if_mgu
303. added lemmas inv_renaming_sound and ex_inverse_of_renaming
304. added lemma subst_apply_term_ident
305. added lemmas subst_range_Var and range_vars_Var and moved stuff around
306. added lemma subst_apply_term_subst_apply_term_eq_subst_apply_term_lhs and tuned naming
307. tuned naming
308. added lemma mgu_range_vars
309. added lemma subst_compose_apply_eq_apply_lhs_if
310. added lemmas is_Var_mgu_if_not_in_equations, ball_is_Var_mgu, and inj_on_mgu
311. RealTimeDeque: replace `reverseN` with `take_rev
312. replaced Open_Induction.Restricted_Predicates.total_on by equivalent HOL.Relation.totap_on
313. merge from afp-2022
314. add missing thy files in Sturm_Tarski + repair
315. afp-submit: style page, improve elements;
316. afp-submit: added repository updates;
317. afp-submit: added download and faster file handling;
318. add submission pages to web ui;
319. afp-submit: add submission and build status with adapter to existing system;
320. add user-facing exception handling to web app;
321. clarified submission handling;
322. afp-submit: added submission read-only and list views;
323. add afp-submit web app;
324. add web app facilities;
325. RealTimeDeque: Separate implementation and auxiliary functions
326. Backed out changeset 3a67df508397 The finite simproc is no longer active by default
327. adapted to new simproc finite
328. clarified signature, following Isabelle/f362975e8ba1;
329. more direct Proof_Context.init_global;
330. proper naming conventions for Isabelle/ML;
331. Updated citation
332. merge from afp-2022
333. Isabelle2022: new release download links
334. Added tag Isabelle2022 for changeset 548e384c0445
335. import 2022 release dates
336. entry names not restricted to alpha-numeric
337. add 2021-1 all releases;
338. clarified docs
339. replace old get-releases tool (now isabelle afp_release -I);
340. add option for parallel session builds
341. set Isabelle2022 release date
342. set release version to 2022
343. merge from afp-2021-1
344. Removal of some old junk
345. Deleted unused material
346. nothing
347. Instantiation of the order solver for ⊑ and ⊏ (no real effect though)
348. proof simplifications
349. merged
350. Simplified the proofs a bit
351. merged
352. replaced fmember.rep_eq by fmember_iff_member_fset
353. merge from afp-2021-1
354. only make parent dir;
355. accept all dois;
356. metadata toml: tuned error messages;
357. clarified sub topics;
358. adapted to Isabelle/457f1cba78fb
359. merged
360. added lemmas generalizes_lit_refl[simp] and generalizes_lit_trans; added simp annotation to generalizes_refl
361. extracted proof cases from lifting_lemma to distinct lemmas
362. tuned proof due to new simp rules
363. corresponding lemma was removed from distribution
364. regen site
365. updates to BenOr_Kozen_Reif by Katherine Kosaian
366. fix author entry; regen website
367. add change history revision
368. Added scene spaces, improvements to prisms, and improvements to the alphabet command.
369. merge from afp-2021-1
370. new entry Query_Optimization
371. remove temp file
372. Complex_Bounded_Operators: Various changes: - Removed auxiliary constant `the_riesz_rep_bilinear'` - Renamed constant `the_riesz_rep_bilinear` -> `the_riesz_rep_sesqui` and defined differently but equivalently - Renamed constant `bifunctional` -> `bidual_embedding` (and renamed lemmas containing `bifunctional` accordingly) - Renamed lemmas `the_riesz_rep_bilinear_apply` -> `the_riesz_rep_sesqui_apply`, `cblinfun_extension_exists_norm` -> `cblinfun_extension_norm_bounded_dense` - New theorems: `rank1_compose_left`, `rank1_compose_right`, `rank1_scaleC`, `rank1_uminus`, `rank1_uminus_iff`, `rank1_adj`, `rank1_adj_iff`, `bidual_embedding_surj`, `Cblinfun_comp_bounded_cbilinear`, `Cblinfun_comp_bounded_sesquilinear`, `bounded_clinear_0`, `bounded_antilinear_0`, `bounded_cbilinear_0`, `bounded_sesquilinear_0`, `bounded_cbilinear_apply_bounded_clinear`, `bounded_sesquilinear_apply_bounded_clinear`, `cblinfun_extension_exists_hilbert`, `trunc_ell2_reduces_norm`, `trunc_ell2_add`, `trunc_ell2_scaleC`, `bounded_clinear_trunc_ell2` - Theorem `cblinfun_extension_exists_proj`: Reformulated one assumption
373. slightly less abusive proof pattern
374. Many changes to entry `Complex_Bounded_Operators`: - Removed all use of deprecated `⟨.,.⟩` syntax for complex inner product. (Now: `∙⇩C`) - Cosmetic changes and cleanup of some proofs - Type class `one_dim` inherits from `complex_inner` now. - Moved various theorems around between theories - Added `[simp]` to: `Proj_partial_isometry`, `cadjoint_id` - Removed theorems: `onorm_Inf_bound`, `norm_unit_sphere` - Changed theorems: `of_complex_cblinfun_apply` (made into more general simp-rule), TODO orthospacething - New definition: `rank1` (and lemmas about it) - New theorems: `one_dim_iso_cblinfun_apply`, `vector_to_cblinfun_one_dim_iso`, `image_vector_to_cblinfun_adj`, `image_vector_to_cblinfun_adj'`, `sgn_cinner`, `orthocomplement_top`, `orthogonal_spaces_ccspan`, `norm_scaleC_sgn`, `one_dim_ccsubspace_all_or_nothing`, `surj_isometry_is_unitary` - Renamed `vector_to_cblinfun_cblinfun_apply` -> `vector_to_cblinfun_cblinfun_compose` (also turned around and added `[simp]`), `cancel_apply_Proj` -> `Proj_fixes_image`, `range_is_clinear` -> `range_is_csubspace`. - Changed definition: `is_Proj` (logically equivalent by `Proj_range_closed`) Fixed entry `Registers` due to the changes above.
375. tuned proofs
376. merge from afp-2021-1
377. new entry Undirected_Graph_Theory
378. typo
379. typo
380. New entry: Maximum_Segment_Sum
381. regenerate site;
382. added topic for data management systems;
383. added missing file
384. New entry Safe_Range_RC
385. adjust Stalnaker_Logic to changes in Epistemic_Logic;
386. adjusted to distribution
387. remove duplicate code;
388. restructure afp ci builds (see Isabelle/3c4e373922ca)
389. Cosmetic changes.
390. merge from afp-2021-1
391. regenerate site;
392. afp site: minor stylistic improvements;
393. web entry for Stalnaker_Logic
394. new entry: Stalnaker Logic
395. clarified options, following f2094906e491;
396. Comments on theories brought from ZF-Constructible. Shortening fm names
397. adjusted to distribution
398. Remove fontenc from root.tex to make Ł show in PDF.
399. Update ROOT...
400. Appendix with another axiom system as a variant of the proof.
401. adapt to Isabelle@769a7cd5a16a
402. merge from afp-2021-1
403. adjust Lar's contact info as requested
404. sitegen for Padic_Field
405. new entry: Padic_Field
406. sitegen for Risk_Free_Lending
407. new entry: Risk_Free_Lending
408. new entry Implicational_Logic
409. New entry Separation_Logic_Unbounded
410. added web files
411. added web files
412. New entry SCC_Bloemen_Sequential
413. A few more disambiguations, related to locales in CartesianCategory.
414. Merged
415. Further disambiguation of facts to address clashes involving ConcreteCategory as a sublocale.
416. streamlined division on polynomials
417. Complex_Bounded_Operators: Fixed errors in document generation
418. Complex_Bounded_Operators: Added numerous new lemmas.
419. Merged
420. Disambiguate sufficiently many facts in locales so as to permit a top-level interpretation of ZFC_set_cat.
421. Fix a typo.
422. Neater links
423. Relational_Disjoint_Set_Forests: variant abstraction
424. merged
425. support for ISABELLE_MLTON_OPTIONS, following Isabelle/d27ed188e0c4;
426. Renaming synthesized formulas
427. prefer (smt (verit)), which is potentially more stable under heavy load;
428. Add additional results.
429. Formatting.
430. Add papers to abstracts.
431. merged
432. Purely cosmetic
433. merged
434. Deleted one redundant step
435. merged
436. Merge
437. Tidied (a lot)
438. added missing congruence rule
439. streamlined
440. tuned proofs (manually or with sledgehammer): avoid "smt" due to spurious failures under heavy load;
441. tuned whitespace;
442. merged
443. some slight polishing in the UTM entry
444. added congruence rule for forallM of Error-Monad
445. updated to devel
446. merged
447. tuned proofs (manually or with sledgehammer): avoid "smt" due to spurious failures under heavy load;
448. removed obsolete workaround (see Isabelle/91ee232b4211);
449. Eliminated the temporary material that was already migrated to the Isabelle libraries
450. merge from afp-2021-1
451. regenerate site;
452. tuned;
453. merged
454. New entry CRYSTALS-Kyber
455. regenerate site;
456. added missing history in metadata;
457. retrieve missing change history in metadata migration tool;
458. backout b2ae7c2c3ea51af8f43b76cdcb5d499c5085e726
459. new email address for Maksym
460. metadata and sitegen for Khovansikii_Theorem
461. new entry: Khovanski-Theorem
462. fixed metadata for Hales_Jewett
463. sitegen for Number_Theoretic_Transform
464. new entry Number_Theoretic_Transform
465. new entry Hales Jewett
466. adapt to only check ROOT for directories in thys (aftermath of Isabelle/a9bbf075f4319e920a22a1c0a5b763b6575f2089);
467. updated entry for Universal Turing Machines
468. merged
469. adapted to antimono
470. merged
471. adapted to new mono and strict_mono
472. updated to Isabelle/5ea588440b06
473. Updated citations
474. Updated citations
475. tuned signature;
476. merged
477. Substantial additions by Franz Regensburger to the Universal_Turing_Machine entry
478. tuned timeouts, based on test runs with threads=1;
479. replaced slow smt call by blast
480. avoid hardwired document;
481. merged
482. cosmetic
483. replace smt_oracle by proper veriT reconstruction
484. merged
485. tweaks
486. make all sessions of chapter "AFP" belong to group "AFP";
487. chapter_definition for presentation;
488. Undo an unrelated change that somehow crept into the previous commit.
489. Remove lots of unnecessary explicit quantifiers in lemma statements, now that I've discovered "arbitrary:".
490. Revised locale structure and notation. Proposed modularization for ZF-Constructible's M_eclose
491. tuning
492. updated entries: Combinatorics_Words, Combinatorics_Words_Lyndon, and Combinatorics_Words_Graph_Lemma
493. avoid fact name clash
494. adjusted to distribution
495. repaired proof
496. Complex_Bounded_Operators: Fixed document generation
497. Merged changes.
498. Registers: Fixed parse error.
499. Misc updates to Complex_Bounded_Operators: Many new lemmas. New definitions: cblinfun_power, cblinfun_left, cblinfun_right, ccsubspace_Times, partial_isometry, the_riesz_rep, the_riesz_rep_bilinear', the_riesz_rep_bilinear, bij_between_bases, unitary_between, is_onb, some_chilbert_basis, rel_ccsubspace. instance prod :: complex_normed_vector. Changed infix priority of oCL to 67. Changed local structure: Complex locales now are sublocales of real locals with prefix real. Renamed norm_blinfun_id_le -> norm_cblinfun_id_le.
500. Reintroduce type signatures.
501. Switch to simultaneous substitutions.
502. merge from afp-2021-1
503. new entry: Nano_JSON
504. sitegen for Commuting_Hermitian
505. new entry: Commuting_Hermitian
506. Sitegen for Involutions2Squares (WITH WRONG EMAIL ADDRESS)
507. new entry Involutions2Squares
508. fix typo
509. new entry Solidity
510. tuned title
511. more typos
512. regenerate because of typos
513. New entry
514. topics no longer exist
515. new topics
516. New entry FSM_Tests
517. merged
518. Isabelle/b6589c8ccadd officially supports README.thy;
519. streamlined
520. tuned proofs
521. discontinued obsolete README.html: superseded by abstract provided by AFP;
522. streamlined primitive definitions for integer division
523. tuned code equations for Xml-parsing
524. refactored algebraic number theories, generalized Cauchy Root Bounds lemma (so that real and complex numbers work)
525. Revision of locale structure
526. Purely markup
527. Fix ImpSplit thy for document generation
528. Add B+Tree formalisation to the BTree entry
529. Correcting thm antiquotations. Turning code comments into text
530. Update metadata and root.tex to mention the addition of ZFC_SetCat in early 2022.
531. Sync with my development repo: Category3: add various rules for limits. RTS: strengthen definition of transformation.
532. adapted to NLists.thy
533. merged
534. use Library/NList.thy now
535. Further streamlining of quick-and-dirty evaluation.
536. An attempt for an integrated solution for quick-and-dirty evaluation.
537. Further reduction of locale assumptions
538. merged
539. more complete theorem_commands;
540. clarified signature, following Isabelle/b6d74c90b588;
541. Update metadata for Frequency_Moments.
542. merged
543. Update Schutz_Spacetime chain (and other) definitions, notations, extra gorder proof, general cleanup corresponds to revisions to JAR paper
544. more accurate name
545. more politically correct
546. two new lemmas
547. added two lemmas to relational chains
548. changed confusing assumption name
549. avoid the surprise that n-m is 0 even if n<m.
550. tuned
551. simplified invar
552. merged
553. simplified
554. update metadata;
555. merged
556. tuned
557. removed a spurious locale parameter -- the same issue probably arises in the pen-and-paper Waldmann et al.
558. removed needless assumption
559. Named intermediate results combinable wands
560. Named intermediate results Package logic
561. added lemma about lazy list chains
562. typo
563. Refining three sessions. * Delta_System_Lemma: Moving results out of the scope of AC. * Transitive_Models: General locale re-engineering. * Independence_CH: specifying finite set of axioms required for forcing CH and ¬CH.
564. Tuned.
565. merged
566. addd DOIs and other metadata links
567. some slight polishing of the definitions
568. added links
569. added metadata links
570. added link
571. added Wiki link
572. added DOIs
573. added DIs
574. added DOIs
575. Added DOIs
576. added DOIs
577. added DOIs
578. merged
579. added DOIs
580. XZ compression for Safe_Distance examples (safes 160 MB!)
581. tuned DOIs
582. added DOIs
583. added DOIs
584. added DOIs
585. added pubs
586. merge from afp-2021-1
587. improve DOI resolving: offline cache and better timeouts;
588. added pubs
589. added DOIs
590. merge from afp-2021-1
591. resolve DOIs in sitegen to formatted citations;
592. removed links from related references;
593. regenerate site;
594. Remove duplication between Universal_Hash_Families (UHF) and Finite_Fields (FF). - Also remove white space in UHF.
595. Update metadata for WOOT_Strong_Eventual_Consistency. - Added corresponding publication in related works. - Added orcid id's of authors.
596. added DOI
597. added DOI
598. merged
599. added orcid
600. added orcid
601. added lemma
602. ORCID for Manuel Eberl
603. merge from afp-2021-1
604. updated help page;
605. clarified doc;
606. name change for Kądziołka
607. updated docs on metadata;
608. adjusted topics and added subject classifications;
609. name change for Kądziołka
610. moved lemma to distribution
611. merge from afp-2021-1
612. added more metadata fields: related references for entries, orcids for authors, and acm/ams subject classification for topics;
613. tuned topics
614. adjusted topics
615. proper license link;
616. tuned;
617. merge from afp-2021-1
618. regenerate site;
619. sitegen: integrate change history and note properly;
620. tuned;
621. clarified homepage urls;
622. remove metadata migration tool;
623. toml parser improvements: comments are now treated as whitespace.
624. clarified metadata loading and added more metadata checks;
625. regenerate site;
626. improve releases view and map correctly to Isabelle version;
627. add missing releases again;
628. merged
629. sitegen for Weighted_Arithmetic_Geometric_Mean
630. new entry Weighted_Arithmetic_Geometric_Mean
631. missing file
632. New entry IMP_Compiler_Reuse
633. Just variable renamings
634. merged
635. Simplified and shortened some proofs
636. moved lemmas to distribution
637. merged
638. tweaked
639. merged
640. a bit of tidying
641. cleanup with global-interpretations and code equations in Simplex_Incremental
642. changed incremental simplex interface: check now always returns a new state, even in unsat-case
643. merge from afp-2021-1
644. Improvements.
645. regenerate site;
646. sitegen: tuned statistics;
647. tuned;
648. sitegen for Boolos_Curious_Inference
649. new entry: Boolos_Curious_Inference
650. website: proper bibtex entries;
651. tuned
652. removed more material now residing in distribution
653. separated non-computable instance of bit comprehension from computable one
654. Small changes.
655. Undo accidental changes.
656. Tuned.
657. tuned -- follow clone in $ISABELLE_HOME/src/HOL/Imperative_HOL/Heap_Monad.thy;
658. minor performance tuning: avoid redundant BigInt construction;
659. prefer self-made Array.T, to avoid problems with ArraySeq in Scala 3;
660. more robust Array.T for Scala 2.13 and 3.x, following Isabelle/ca450d902198;
661. Move code lemmas for symbolic computation of bit operations on int to distribution.
662. renamings
663. Relational_Disjoint_Set_Forests: improved abstractions
664. Simplified a proof using Cauchy–Schwarz
665. removed precondition in det_four_block_mat
666. merge
667. removed assumption in det_bound_hadamard_tight, moved some basic lemmas on matrices, added a conditional version of det(four_block_mat ...) = ...
668. merge from afp-2021-1
669. updated doc;
670. regenerate site;
671. obfuscate email addresses in metadata and generated site;
672. renamed det_bound_gram to det_bound_hadamard, showed that bound is tight (using unproven fact about determinants of block-matrices)
673. added lemma for special case of small integer solutions (no mixed integer), where then everything is of type int
674. document change in metadata
675. generalized fixed bounds on determinants to predicate; added an improved determinate bound -> result: get smaller bound on mixed integer solutions (replace n! by sqrt(n^n))
676. Code generated in the same directory
677. Removed ML code from AFP entry
678. adapted to scala-3.1.2;
679. merge from afp-2021-1
680. tuned;
681. tooling: added utility to check for metadata consistency;
682. regenerate website;
683. site: generate multi-line json for smaller merges;
684. toml module: proper parsing of quotes in multiline strings;
685. added further sitegen generated websites
686. added metadata for Real_Time_Deque's, sitegen
687. new entry: Real-Time Double-Ended Queue
688. merged
689. replaced IMGU by min_IMGU
690. replaced MGU by IMGU
691. exposed that inverse of renaming only maps variables to variables
692. added the r{n..} regular expression to the extensions directory in the Posix-Lexing entry, added two small lemmas to the Regular-Set theory
693. merge from afp-2021-1
694. regenerate website
695. do not ignore admin/site
696. remove afp python component build tool;
697. afp tooling: improve keyword extraction;
698. website: small improvements;
699. tuned efficiency of XML parser
700. tuned
701. updated the abstract in root.tex
702. added the r{..n} regular expression to the extensions directory
703. merged
704. tuned BNF bound
705. strict bounds for BNFs (by Jan van Brügge)
706. merge from afp-2021-1 (replaying devel commit)
707. replaced python RAKE component with Isabelle/Scala Rake component;
708. remove scala tools from publish;
709. replaced python RAKE component with Isabelle/Scala Rake component;
710. merged
711. avoid hardwired pdf;
712. adapted to Isabelle/986506233812;
713. merged
714. added an implementation of pseudo remainder sequences for calculating Tarski queries
715. merged
716. updated to Isabelle/3c544d64c218
717. merge from afp-2021-1
718. tuned error messages;
719. mention error location when metadata loading fails;
720. merged
721. even more IsaNet;
722. afp metadata/releases: change format to re-add releases swallowed by key-set, remove extra releases;
723. more IsaNet
724. New entry IsaNet
725. adapted to Isabelle/39df30349778;
726. added extension that deals with the n-times regular expression in Posix-Lexing
727. Avoid calculations where not necessary.
728. used long version of definition to avoid conflict when introducing HOL.monotone_on
729. merge from afp-2021-1 (metadata consolidation)
730. sitegen
731. unified home pages
732. re-introduce accidentally reverted changes
733. ignore dev site output
734. consolidate metadata (email and homepages)
735. merge from afp-2021-1
736. load mail configuration lazily (initialized later from properties);
737. tuned home pages
738. merge from afp-2021-1
739. tuned;
740. proper topics loading;
741. merge from afp-2021-1 (new website)
742. new website
743. admin: remove old sitegen lib files
744. update metadata to new sitegen
745. merge website-redesign graft
746. updated afp sitegen doc;
747. replaced python afp stats with Isabelle/Scala tool;
748. updated afp metadata doc (now as markdown);
749. afp components: removed unnecessary platforms;
750. afp sitegen: switch to new version;
751. add sitegen ignore option;
752. improvements for toml module: proper boolean values;
753. add components as proper afp deps;
754. tuned;
755. switched to standalone cross-platform afp python component;
756. tuned;
757. afp python build: use tgz for better cross-plattform compatability;
758. replaced ci_profiles by statically compiled afp_build tool (Scala 3 preparations);
759. afp structure: added accessors;
760. hugo site: minor changes;
761. hugo-site: improve various aspects;
762. add new authors to migration;
763. clarified formatting, for the sake of scala3;
764. hugo site: better scrolling;
765. hugo site: updated devel info;
766. hugo site: updated content;
767. hugo site: proper ordering;
768. hugo site: restricted generated affiliations; hugo site: added fresh option;
769. hugo site: proper theory view link scrolling;
770. hugo site: tuned affiliation keys;
771. hugo site: proper topic-only topics page;
772. hugo site: relativize paths;
773. hugo site: list sessions separately;
774. hugo site: tuned;
775. hugo site: tuned;
776. hugo site: merge gen and build tool;
777. hugo site: added doc headers;
778. hugo site: tuned;
779. afp metadata: index keys for emails and urls; apf metadata: separate license file;
780. hugo site: improve theory view;
781. hugo site: cleaned up;
782. hugo site: added devel version;
783. hugo site: updated search and content;
784. hugo site: added theory view styling for different device sizes; hugo site: update contributions;
785. Updated metadata in migration and theory view;
786. hugo site: updated site templates;
787. metadata migration: updated authors;
788. hugo: added mobile view;
789. hugo: copy to proper path;
790. added theory navbar;
791. tuned formatting;
792. added loader;
793. tuned;
794. tuned: more canonical Isabelle code style;
795. proper loading of foundational hrefs;
796. fix dependencies;
797. added devel flag;
798. updated about page;
799. moved extraction of related entries to hugo;
800. improved keyword extraction;
801. added keywords to site generated entry data;
802. use tmp file for python script instead of command;
803. added js-side theory loading to afp site;
804. integrated metadata changes into site; tuned;
805. added missing keyword data;
806. removed html dir from sitegen (now set inside hugo);
807. tuned sitegen: moved dependencies generation to scala
808. changed generated author format;
809. tuned;
810. tuned;
811. tuned hugo: static files more explicit;
812. tuned;
813. proper authors/affiliations gen for hugo taxonomy;
814. clarified hugo data;
815. added missing name mapping to migration;
816. proper output path;
817. added missing topics;
818. clarified hugo build signature; split site generation into own afp site gen tool;
819. added more steps to afp site generation tool;
820. tuned; clarified hugo;
821. added hugo project by Carlin MacKenzie;
822. added sitegen scripts by Carlin MacKenzie (slightly tweaked);
823. added afp hugo module;
824. clarified afp_dependencies: proper typed output; added afp_dependencies json module;
825. Added afp structure module;
826. Added python wrapper;
827. clarified metadata;
828. tuned;
829. added afp hugo component;
830. added afp python component with required packages;
831. feat(afp/tools): added initial site build tool
832. tuned(afp/tools): metadata sorted
833. tuned(afp/tools): tuned parser/unparser
834. feat(afp/tools): more metadata and toml conversion;
835. feat(afp/tools): added TOML lexer and parser;
836. tuned(afp/tools): module jar locations;
837. fix(afp/tools): added missing metadata, improved toml structure
838. fix(afp/tools): removed TOML formatting heuristics for simplicity;
839. feat(afp/tools): added TOML module;
840. feat(afp/tools): added metadata migration tool;
841. feat(afp/tools): migrated scala tool_bodys to proper tools;
842. Avoid explicit operation when not necessary.
843. adjust for isabelle@5bba3516ddb5
844. merge from afp-2021-1
845. Added a missing acknowledgement
846. metadata for Finite_Fields (and missing <> for two previous entries)
847. new entry: Finite_Fields
848. sitegen for DPRM_Theorem
849. DPRM_Theorem: finally cleaned up and impressive!
850. New entry [Rewrite_Properties_Reduction]
851. Fixed broken LaTeX in the abstract
852. sitegen for Combinable_Wands
853. New entry Combinable_Wands
854. corrected metadata (separate authors by "," not by "and")
855. sitegen and metadata for Pluennecke_Ruzsa_Inequality
856. new entry: Pluennecke Ruzsa Inequality
857. Tuning the abstract to remove some of the display mathematics
858. sitegen for Package_logic
859. new entry Package_logic
860. Removal of all email addresses, at authors' request
861. renamed some variables
862. proper \open\close markup
863. Updated the Posix-Lexer entry including a small change in Regular-Set
864. Trimmed down dependencies.
865. Merge equivalent instance declarations for functions in Lp.Functional_Spaces and HOL-Library.Function_Algebras. Because of the distinct but equivalent instance declarations in the mentioned theories, it was not possible to import both libraries at the same time. This commit fixes the problem.
866. Remove duplicate lemma and fix typos in Frequency_Moments.
867. same variant as for imperative algorithm to prove n^2 complexity
868. tuned
869. Shortened and simplified a proof
870. more realistic timeout;
871. tuned whitespace;
872. more realistic timeout; more parallelism;
873. avoid hard-wired document;
874. removed usages of HOL.no_atp as its content and order is not guaranteed
875. cleaning
876. no separate code-equations required for a lift_definition by using (code_dt) instead
877. The last few occurrences of integrable_cong
878. Tidying/removal of obsolete material
879. Fixed a use of Bochner_Integration.integrable_cong
880. fixes for compatibility with renamed / new lemmas
881. Tiny simplifications
882. A tiny bit of reorganisation
883. the last "simp/auto" problems
884. corrected all "bysimp"
885. Automated merge with bundle:/var/folders/9z/l1x9y3bd16x9_70pdp4703jr0000gp/T/SourceTreeTemp.3gPj1U
886. Tidied auto/simp with null arguments
887. merged
888. comleted single loop refinement
889. minor adjustments
890. metadata
891. minor amendments
892. creation and preservation of limits; a variety of auxiliary results and amendments
893. patched a broken proof
894. merged
895. single lopp variant refined to lists.
896. adjust for isabelle@7095df141819
897. merge from afp-2021-1
898. typo fix
899. sitegen for Digit_Expansions
900. New entry Digit_Expansions
901. finally!!!! Sitegen for Sophomore's Dream
902. merged
903. Minor corrections to metadata (no "and" between authors' names)
904. Updating the version of Jinja2, as suggested by Manuel
905. merged
906. updated metadata
907. new entry Sophomores_Dream
908. updated name and email address of Rose Bohrer
909. sitegen for Clique_and_Monotone_Circuits
910. new entry Clique_and_Monotone_Circuits
911. metadata and sitegen for Fisher's inequality
912. new entry: Fisher's Inequality
913. New entry Multiset_Ordering_NPC
914. sitegen for Frequence_Moments
915. new entry: Frequence_Moments
916. metadata and sitegen for Prefix_Free_Code_Combinators
917. new entry: Prefix_Free_Code_Combinators
918. regen website (some orders are different in python3)
919. switch sitegen to python3
920. sitegen for new entry
921. new entry: FOL_Seq_Calc3
922. New entry: Dedekind_Real
923. New entry Ackermann_not_PR, from distribution
924. Cotangent_PFD_Formula sitegen
925. new entry Cotangent_PFD_Formula
926. website for Independence_CH
927. new entry Independence_CH
928. New entry ResiduatedTransitionSystem
929. Transitive_Models webpage
930. new entry Transitive_Models
931. updated name and email address of Rose Bohrer
932. Removal of unnecessary material
933. perfectly pointless streamlining
934. More general definition of gcard
935. refined one-loop version further
936. tidied up a few proofs
937. A bit of beautification
938. Yet more tidying and streamlining of graph lemmas
939. merged
940. A few trivial changes
941. Tweaks concerning the versions of Zhao's evolving lecture notes
942. Trying to simplify a bit more
943. More simplification of proofs. Removal of numeric references to Zhao.
944. tidying and simplification
945. merged
946. More purely cosmetic changes
947. moved from AFP to distribution
948. tuned syntax
949. simplified some proofs and deleted quite a bit of redundant material
950. Shorter proofs and leaner notation.
951. Minor updates supplied by the author, mostly connected with a reference to a work by Hilbert, now deleted.
952. Add a construction, using ZFC_in_HOL, of the category of small sets and functions.
953. Resolve a "Duplicate constant declaration" issue that occurs with "isabelle build -o export_theory".
954. avoid side effects on working copy while runnign sessions (generated code is unused)
955. clarified formatting, for the sake of scala3;
956. Deleted a few redundant lines
957. Trying to beautify this, but it's still ugly
958. And a bit more tidying
959. more renaming and tidying
960. Alphabetic substitutions
961. Eliminated another finiteness assumption
962. Removal of some needless finiteness assumptions
963. Removed a small amount of redundant material from both Szemerédi and Roth
964. merged
965. tidied up a few proofs
966. A slightly nicer proof
967. merged
968. tidied and generalised some proofs using small_eqpoll
969. merged
970. tidied some proofs
971. Improved handling splitting theorems in the alphabet command
972. Fixed wrong sign handling in fmul-add
973. more count_list lemmas
974. more count_list
975. merged
976. moved some count_list lemmas
977. synchronize with https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/tree/5f38d029bfcabac8ba3b4ceea747f07772d1390d
978. synchronize with https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/tree/5f38d029bfcabac8ba3b4ceea747f07772d1390d
979. synchronize with https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/tree/5f38d029bfcabac8ba3b4ceea747f07772d1390d
980. synchronize with https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/tree/5f38d029bfcabac8ba3b4ceea747f07772d1390d
981. continue 98838b260ed4
982. continue ee01bce2ecca
983. cancel some part of 11d4567f1b99
984. cancel some part of 98838b260ed4
985. cancel some part of ada85c62541d
986. synchronize with https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/tree/5f38d029bfcabac8ba3b4ceea747f07772d1390d
987. split locale in two
988. Stronger strong completeness result and variant that uses variables as Henkin witnesses.
989. Stronger strong completeness result and variant that uses variables as Henkin witnesses.
990. added some alternative proofs in Smith_Normal_Form entry
991. The last tranche of material to be moved to the complex analysis libraries
992. Removal of material that has since been added to ZFC_in_HOL.General_Cardinals
993. Deleted nearly 200 lines of unused material
994. A new theorem
995. Clarified code module names.
996. removed ancient numeral representation
997. restore state of VYDRA_MDL to b8c3f69745a4
998. merge from afp-2021-1
999. metadata for Universal_Hash_Families
1000. new entry Universal_Hash_Families
1001. New entry Wetzel's Problem
1002. metadata for Eval_FO
1003. new entry Eval_FO
1004. metadata for VYDRA_MDL
1005. new entry VYDRA_MDL
1006. Backed out changeset c9f94b0ae10e
1007. Backed out changeset b8c3f69745a4
1008. metadata update for VYDRA_MDL
1009. New entry: VYDRA_MDL
1010. fixed failing proofs
1011. New definition of the Aleph operator so that it's defined for all arguments, not just ordinals
1012. ALEXANDRIA acknowledgements
1013. merged
1014. New set theory lemmas about cardinality (mainly)
1015. Another attempt for a consolidated terminology.
1016. Avoid overaggresive splitting.
1017. more lemmas for distribution
1018. Avoid overaggresive simplification.
1019. some new lemmas
1020. merged
1021. More material
1022. added idempotent most general unifier
1023. used same parameter order for locales substitution and substitution
1024. patched for new/simplified lemmas
1025. Better notation.
1026. merge from afp-2021-1
1027. avoid conflict with index.html in generated html
1028. New entry: FO_Theory_Rewriting
1029. Improve consistency of type-variables in WOOT_Strong_Eventual_Consistency. + Remove obsolete e-mail from notification mailing list.
1030. Improve proofs for Interpolation_Polynomials_HOL_Algebra. Reduced the number of apply scripts used.
1031. Correct date.
1032. deleted a lemma that's in the devel library
1033. Cleanup and new results.
1034. moved theorems into Matrix.thy
1035. merge of AFP 2021-1
1036. New AFP entry: Equivalence_Relation_Enumeration
1037. new entry: LP_Duality
1038. cosmetic tweaks
1039. sitegen and metadata for Young's inequality
1040. new entry: Young's inequality
1041. metadata for Quasi_Borel_Spaces, sitegen
1042. new entry: Quasi_Borel_Spaces
1043. sitegen for FOL_Seq_Calc2
1044. new entry FOL_Seq_Calc2
1045. tweak: corollary that the ln also yields irrational numbers
1046. New entry: Interpolation_Polynomials_HOL_Algebra
1047. Finally remembered to run sitegen
1048. Fixed the meta data in the abstract as well
1049. Eliminated the references to SOS (which is no longer used) and changed to the document style to "article".
1050. typo
1051. typo
1052. New entry Irrationals_From_THEBOOK
1053. new entry Median_Method
1054. Actuarial Mathematics website
1055. New entry Actuarial_Mathematics
1056. Strong soundness.
1057. Strong soundness.
1058. Fix LaTeX issue.
1059. Qualification required(?)
1060. merged
1061. more variants of the algorithm
1062. Added funding acknowledgments. Fixed broken BibTeX citation.
1063. Strong completeness for PAL systems.
1064. Cleanup.
1065. Fewer parentheses around turnstile + remove unused lemmas.
1066. Simplify proof of truth lemma.
1067. Notation for `imply` and fewer parenthesis around turnstiles.
1068. Abstract results to shorten proofs.
1069. Better notation.
1070. merged
1071. tuned whitespace;
1072. more symbols;
1073. profer bundle lattice_syntax;
1074. prefer existing lattice_syntax and no_lattice_syntax, with proper 'no_notation' as intended;
1075. Add soundness and completeness for the PAL versions of systems K, T, KB, K4, S4 and S5.
1076. avoid hardwired document output;
1077. merged
1078. deleting the overloading of div and mod, with its attendant ambiguities
1079. replaced Erdős by Erd\H{o}s (fixed problem in LaTeX document generation)
1080. Removal of a lemma (now in the libraries) and a few tweaks
1081. Tuning.
1082. merged
1083. tweaks
1084. merged
1085. Fixed an inadequate description
1086. tuned
1087. mv to distribution
1088. by now in distribution
1089. merge from afp-2021-1
1090. fixed abstract
1091. tuned
1092. website and metadata for Hyperdual
1093. new entry: Hyperdual
1094. sorted ROOTS
1095. tuned
1096. New entry Knights_Tour
1097. more thoroughly replace Michael Foster's e-mail address
1098. metadata and sitegen for Gale_Shapley
1099. new entry Gale_Shapley
1100. update Michael Forster's email address
1101. metadata and sitegen for Roth_Arithmetic_Progressions
1102. new entry Roth_Arithmetic_Progressions
1103. typo
1104. merged
1105. New entry Regular_Tree_Relations
1106. We DON'T want an output directory
1107. MDP-Algorithms website
1108. new entry MDP-Algorithms
1109. typo
1110. new entry MDP-Rewards
1111. fixed typo
1112. CS: possibility to disable backtracking; CZH: auxiliary results; ETTS: minor amendments
1113. used wfP_imp_asymp from HOL
1114. simplified proof some more
1115. simplified proof
1116. Extended protocol model to support composition of more than two protocols without the need of re-labeling them, additional automated checks, tighter integration of the stateful protocol model and the automated verification (PSPSP) tool.
1117. Tweaked some failing proofs
1118. adapted to new Sledgehammer.run_sledgehammer return type
1119. Strengthened a lemma
1120. updated the definition of scheme
1121. merge from afp-2021-1
1122. add change history
1123. updated 2021-1 release dates -> web
1124. merge from afp-2021-1
1125. ignore generated files
1126. add 2021-1 release dates
1127. set devel version again
1128. Added tag Isabelle2021-1 for changeset 11f8b03a88ad
1129. adjust usage version
1130. set release version
1131. update release dates
1132. merge from afp-2021-1
1133. The version without integer indexes
1134. The version without integer indexes
1135. merge from afp-2021-1
1136. merge from afp-2021
1137. new entry Foundation_of_geometry
1138. merge from afp-2021-1
1139. Modified all design locale parameters to be nats instead of ints. Fixed proofs as required.
1140. adjust for Isabelle2021-1-RC5
1141. merge from afp-2021
1142. new entry Simplicial_complexes_and_boolean_functions
1143. Modified all design locale parameters to be nats instead of ints. Fixed proofs as required.
1144. merge from afp-2021-1
1145. adjust to Isabelle2021-1-RC5
1146. merge from afp-2021
1147. metadata and sitegen for Hahn_Jordan_Decomposition
1148. added Mathematics/Measure theory
1149. new entry: Hahn_Jordan_Decomposition
1150. New entry: Van_Emde_Boas_Trees
1151. New entry: Van_Emde_Boas_Trees
1152. metadata and sitegen for SimplifiedOntologicalArgument
1153. new entry: SimplifiedOntologicalArgument
1154. Tuned: use a star in witness.
1155. Rename H to S in maximal_exactly_one.
1156. Get rid of the sat abbreviation.
1157. Add missing spaces in semantics_tm.
1158. No space in front of object-logic forall.
1159. Non-conflicting name for boolean denotation.
1160. Simpler Hintikka definition.
1161. Add syntactic abbreviation for constants.
1162. Add papers to metadata.
1163. In the definition of regular pair, switched from strict to non-strict
1164. A slightly stronger lemma allowing slightly simpler proofs
1165. merged
1166. generalized standard formula redundancy out of standard redundancy
1167. merged
1168. discontinued Parse.text;
1169. discontinued old-style {* verbatim *} tokens;
1170. weakened locale assumptions: wfP implies asymp
1171. Add papers to metadata.
1172. refactored Standard_Redundancy_Criterion to not use ordering type classes
1173. isabelle update_cartouches;
1174. removed obsolete "extend" operation;
1175. more symbolic latex_output via XML (using YXML within text); re-use existing Latex.output_markup;
1176. prefer symbolic Latex.environment (typeset in Isabelle/Scala);
1177. tuned signature;
1178. feat(Auto2_HOL) fix setup such that auto2 can be used by other object logics and multiple times
1179. Tuned: use a star in witness.
1180. merge from afp-2021-1
1181. adjust for new tags in Isabelle2021-1-RC4
1182. fix dangerous context management
1183. In the definition of regular pair, switched from strict to non-strict
1184. Rename H to S in maximal_exactly_one.
1185. Get rid of the sat abbreviation.
1186. Add missing spaces in semantics_tm.
1187. No space in front of object-logic forall.
1188. Non-conflicting name for boolean denotation.
1189. Simpler Hintikka definition.
1190. Add syntactic abbreviation for constants.
1191. fixed lemma following Isabelle/c256bba593f3