diff options
| author | Josh Chen | 2018-08-08 10:35:43 +0200 |
|---|---|---|
| committer | Josh Chen | 2018-08-08 10:35:43 +0200 |
| commit | 25225e0c637a43319fef6889dabc222df05bfd3c (patch) | |
| tree | e3756da3c360692287ce508c1268314010c3a854 /HoTT_Methods.thy | |
| parent | ec8e1d9d245950f185f6d4ff1b5e1b8755e7202c (diff) | |
Rewriting projection functions
Diffstat (limited to 'HoTT_Methods.thy')
| -rw-r--r-- | HoTT_Methods.thy | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index 8a4417d..8351c3c 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -57,9 +57,9 @@ method derive uses lems unfolds = ( unfold unfolds | simple lems: lems | match lems in lem: "?X : ?Y" \<Rightarrow> \<open>wellformed jdgmt: lem\<close> | - rule Universe_hierarchy | - (rule Universe_cumulative, simple lems: lems) | - (rule Universe_cumulative, match lems in lem: "?X : ?Y" \<Rightarrow> \<open>wellformed jdgmt: lem\<close>) + rule U_hierarchy | + (rule U_cumulative, simple lems: lems) | + (rule U_cumulative, match lems in lem: "?X : ?Y" \<Rightarrow> \<open>wellformed jdgmt: lem\<close>) )+ |