#
2ef30af3 |
|
16-May-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix examples/lambda/typing for tight equality
|
#
cad894cc |
|
20-Sep-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix lambda/typing example given 'perm_type' changes.
|
#
bc294d17 |
|
02-Sep-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Extract a usable half-way point from nominal_datatype branch. This replaces the is_perm predicate with a type embodying that predicate. It doesn't include the subsequent work on allowing multiple 'atom' types.
|
#
effc431b |
|
01-Oct-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Change export_rewrites back to its old API (without requiring an extra string). When exported, the resulting simpset fragment always picked up the name of the theory to be the base of its name, so there didn't seem much point in giving users a false impression of naming power.
|
#
1f53b889 |
|
30-Aug-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Refactor simple type theory development by moving theory of contexts as association lists on strings to a separate theory.
|