C

core-to-isabelle

Settings | Report Duplicate

0

I Use This!

Inactive

Commits : Listings

Analyzed 1 day ago. based on code collected 1 day ago.

Commit Message	Contributor	Files Modified	Lines Added	Lines Removed	Code Location	Date
Dec 07, 2024 — Dec 07, 2025 Showing page 1 of 5 Search / Filter on:
add simp rule for case expressions on lambdas	Brian Huffman	More...				over 13 years ago
add procedure for simplifying case expressions with wildcards	Brian Huffman	More...				over 13 years ago
simprocs for comparisons and case expressions can now prove inequalities of constructor tags	Brian Huffman	More...				over 13 years ago
add simp rules for case expressions	Brian Huffman	More...				over 13 years ago
hide duplicate constant names from the HOL library	Brian Huffman	More...				over 13 years ago
halicore_data generates is_constructor lemmas for use with simprocs	Brian Huffman	More...				over 13 years ago
update comment documenting halicore_fun	Brian Huffman	More...				over 13 years ago
add simprocs for reasoning about data constructors (from July 2011)	Brian Huffman	More...				over 13 years ago
add definition for constant 'undefined'	Brian Huffman	More...				over 13 years ago
declare more simp rules	Brian Huffman	More...				over 13 years ago
Halicore_Terms.thy: new theory with hybrid syntactic/denotational model; Eventually this will replace the current Halicore_Defs.thy.	Brian Huffman	More...				about 14 years ago
Halicore_Type_Meaning.thy: completely revised and updated	Brian Huffman	More...				about 14 years ago
fix incorrect Isabelle2011-1 adaptation: install typecheck as global solver	Brian Huffman	More...				about 14 years ago
Defl_Lib.thy: add deflation combinator for dependent strict function space	Brian Huffman	More...				about 14 years ago
move some theorems	Brian Huffman	More...				about 14 years ago
adapt theory files to Isabelle2011-1	Brian Huffman	More...				about 14 years ago
Halicore_Type_Deep.thy: fix broken comment	Brian Huffman	More...				about 14 years ago
Halicore_Type_Deep.thy: combine TyRec and TyFix into one parameterized constructor	Brian Huffman	More...				about 14 years ago
Halicore_Type_Deep.thy: removed unused string tag on TyData constructor	Brian Huffman	More...				about 14 years ago
Halicore_Kind.thy: add type combinator Tdata, for datatypes	Brian Huffman	More...				about 14 years ago
Halicore_Kind.thy: proof automation for kcont predicate	Brian Huffman	More...				about 14 years ago
Merge branch 'master' of github.com:atomb/core-to-isabelle	Brian Huffman	More...				about 14 years ago
Halicore_Type_Deep.thy: tuned some proofs	Brian Huffman	More...				about 14 years ago
rename core2isa to hcr2thy	Jason Dagit	More...				over 14 years ago
bug fixes for trailing spaces and now we omit the optional case scrutinee expression	Jason Dagit	More...				over 14 years ago
Merge with Aaron and fix zencoding regression	Jason Dagit	More...				over 14 years ago
add a swapped type example	Jason Dagit	More...				over 14 years ago
Change the translator back to using extcore	Jason Dagit	More...				over 14 years ago
Remove problematic ADTs from MultipleDefinitions.	Aaron Tomb	More...				over 14 years ago
Print [] and : as Nil and Cons in expressions.	Aaron Tomb	More...				over 14 years ago

←
1
2
3
4
5
→