C

core-to-isabelle

Settings | Report Duplicate

0

I Use This!

Inactive

Commits : Listings

Analyzed about 15 hours ago. based on code collected about 15 hours ago.

Commit Message	Contributor	Files Modified	Lines Added	Lines Removed	Code Location	Date
Dec 10, 2024 — Dec 10, 2025 Showing page 3 of 5 Search / Filter on:
Add support for non-recursive let expressions in Isabelle/Halicore.	Brian Huffman	More...				over 14 years ago
Renamed many Halicore constants according to a new naming scheme. Each combinator begins with a capital letter that indicates its return type.	Brian Huffman	More...				over 14 years ago
Updates from Hacking session. Lots of little changes, and now the example Translator now supports simple function definitions.	Jason Dagit	More...				over 14 years ago
Halicore_Syntax: fix print rule for case expressions to avoid extra type quotes	Brian Huffman	More...				over 14 years ago
halicore_data now automatically generates parse rules for case expressions	Brian Huffman	More...				over 14 years ago
IsaMakefile: dependencies on *.ML	Brian Huffman	More...				over 14 years ago
add Makefile for examples directory	Brian Huffman	More...				over 14 years ago
Add a simple tree data type example	Jason Dagit	More...				over 14 years ago
Moved isa/examples/ to examples/	Brian Huffman	More...				over 14 years ago
halicore_data: define constants of type string for constructor tags	Brian Huffman	More...				over 14 years ago
halicore_data: refactoring	Brian Huffman	More...				over 14 years ago
halicore_data now generates typing rules for constructor functions	Brian Huffman	More...				over 14 years ago
rename wrongly-named lemma cont_T_abs to cont_T_lam	Brian Huffman	More...				over 14 years ago
halicore_data now generates has_constructor rules for datatypes	Brian Huffman	More...				over 14 years ago
IsaMakefile: remove broken explicit dependency on HOLCF heap image	Brian Huffman	More...				over 14 years ago
halicore_data now generates applied forms of unfold rules (named *_unfold)	Brian Huffman	More...				over 14 years ago
use has_constructor lemmas to prove typing rules for data constructors	Brian Huffman	More...				over 14 years ago
linux installation instructions for Isabelle/Halicore	Brian Huffman	More...				over 14 years ago
renamed isar-keywords.el to isar-keywords-halicore.el	Brian Huffman	More...				over 14 years ago
halicore_data now defines constants for data constructors	Brian Huffman	More...				over 14 years ago
halicore_fun: move code to function.ML; generate definitions for constants	Brian Huffman	More...				over 14 years ago
Halicore_Commands.thy: initial version of "halicore_fun" (does nothing)	Brian Huffman	More...				over 14 years ago
isar-keywords.el: add "halicore_fun" keyword	Brian Huffman	More...				over 14 years ago
Add a readme	Jason Dagit	More...				over 14 years ago
halicore_data now proves continuity and unfold theorems for datatypes	Brian Huffman	More...				over 14 years ago
Halicore_Commands.thy: update description of halicore_data	Brian Huffman	More...				over 14 years ago
Examples.thy: add kind annotation to forall-type	Brian Huffman	More...				over 14 years ago
Halicore_Syntax: print translations to show kind annotations when needed; forall types now default to kind * when no annotation is given	Brian Huffman	More...				over 14 years ago
halicore_data now defines a constant for each datatype	Brian Huffman	More...				over 14 years ago
halicore_data: generate rhs terms for recursive datatype definitions	Brian Huffman	More...				over 14 years ago

←
1
2
3
4
5
→