65 Commits (master)
 

Author SHA1 Message Date
Achim D. Brucker 76b983012d Added reminder to move configuration to Isabelle/Isar. 7 months ago
Achim D. Brucker 961f906944 Fixed typo. 7 months ago
Achim D. Brucker 5288db2205 Fixed typo. 7 months ago
Achim D. Brucker 9c4a2d9483 Integrated fxp and ml_yacc_lib. 7 months ago
Achim D. Brucker 012afeb0a4 Initial commit: ml-yacc support for Isabelle. 7 months ago
Achim D. Brucker 01d66798d3 Initial commit. 7 months ago
Achim D. Brucker 46af09bc1f Changed ref to Unsynchronized.ref. 7 months ago
Achim D. Brucker 69277ff885 Cleanup. 7 months ago
Achim D. Brucker 1d840722d6 Import of fxp sources, as used in su4sml <https://git.logicalhacking.com/HOL-OCL/su4sml>. 7 months ago
Achim D. Brucker b5f15612a7 Upgrading to Isabelle 2020. 9 months ago
Achim D. Brucker ecbfbe0c64 Switched trunk to Isabelle 2020. 2 years ago
Achim D. Brucker f2566edeec Initial commit: SML Code Reflection 2 years ago
Achim D. Brucker 76ab611c86 Port to Isabelle 2019. 2 years ago
Achim D. Brucker faae943ad9 Fixed serializer for definitions using equality from Pure. 3 years ago
Achim D. Brucker 05741ac245 Improved representation of IEEE reals. 3 years ago
Achim D. Brucker dd8a141d5d Code improvement: use actual proof context. 3 years ago
Achim D. Brucker 446792928e Move theory file name from the level of sections to the level of chapters. 3 years ago
Achim D. Brucker eacb55c43f Added Jenkins CI configuration. 3 years ago
Achim D. Brucker 1a88f7c6c3 Added inline Changelot to each theory file. 3 years ago
Achim D. Brucker b0f0d93440 Initial document generation support. 3 years ago
Achim D. Brucker ac1cc224b3 Added brief description of Nano JSON. 3 years ago
Achim D. Brucker 229d3145a5 Initial commit. 3 years ago
Achim D. Brucker 5346943a2b Added Nano_JSON.thy. 3 years ago
Achim D. Brucker 64055200c6 First serializer implementation. 3 years ago
Achim D. Brucker 41634c70ac Added parser and overall cleanup. 3 years ago
Achim D. Brucker 338dcc874a Added serializer implementation. 3 years ago
Achim D. Brucker 1be7bfd514 Defined HOL and ML data types for Nano JSON and implemented conversion between them. 3 years ago
Achim D. Brucker c9a174bdbc Initial commit. 3 years ago
Achim D. Brucker f8f04dd867 Updated various legacy notations. 3 years ago
Achim D. Brucker 818438f2cf Isabelle 2018 is now the default version for the master branch. 3 years ago
Achim D. Brucker bf691e04a0 Fixed markdown. 3 years ago
Achim D. Brucker 4fe36e9ad4 Fixed markdown. 4 years ago
Achim D. Brucker 8a5e954215 Prefixed examples to avoid naming conflicts with consuming theories. 4 years ago
Achim D. Brucker a069d566f8 Bug fix: wrong order of default variables. 4 years ago
Achim D. Brucker 09aa5120f5 Renamed ._ (_.) to .._ (_..) to avoid conflict with common match pattern. 4 years ago
Achim D. Brucker ec1db40bd9 Renamed example definitions to avoid name clashes with consuming theories. 4 years ago
Achim D. Brucker e53d1bcb01 Renamed symtab storing tvar information. 4 years ago
Achim D. Brucker 479c60b2f3 Added input syntax for specifying the last type variable of a type constructor. 4 years ago
Achim D. Brucker d0fc49b78c Improved documentation. 4 years ago
Achim D. Brucker 45e55cf4e7 Implemented possibility to specify a sort (type class) for default variables. 4 years ago
Achim D. Brucker ce7e3896b3 Fixed markdown. 4 years ago
Achim D. Brucker 868cfc53a3 Added reference to the isabelle-hacks repository. 4 years ago
Achim D. Brucker 39ca1b5dc0 Moved hide_tvar_subst_ast_tr into structure Hide_Tvar. 4 years ago
Achim D. Brucker b493001ea6 Added asserts for type variable customization. 4 years ago
Achim D. Brucker 251414e8b4 Cleanup of parse translation hide_tvar_subst_ast_tr. 4 years ago
Achim D. Brucker 3c1b07e065 Introduced ._ and _. notation to override first/last default type variables. 4 years ago
Achim D. Brucker 54d9b20cc4 Implemented print mode (only apply print translation if default types match). 4 years ago
Achim D. Brucker 66307c1c2b Made top-level user interface more consistent. 4 years ago
Achim D. Brucker 92ea551113 Support type synonyms as output notation. 4 years ago
Achim D. Brucker 66101d2527 Changed styntax for type wildcard from __ to (_). 4 years ago