aboutsummaryrefslogtreecommitdiff
path: root/hott/Nat.thy
diff options
context:
space:
mode:
authorJosh Chen2020-05-25 15:24:20 +0200
committerJosh Chen2020-05-25 15:24:20 +0200
commit8f47d9f3ca38a3fc2c3c462d1157866081102ce1 (patch)
tree460181389821f3286fc7082214629817d6ad3427 /hott/Nat.thy
parent3de65af4b59e6d3cc8e74acecf704beccd54b774 (diff)
1. equality method now uses general elimination tactic. 2. New constant `` refers to rhs of equalities.
Diffstat (limited to '')
0 files changed, 0 insertions, 0 deletions