From e1be5f97bb2a42b3179bc24b118d69af137f8e5d Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sat, 18 Aug 2018 21:28:21 +0200
Subject: Regrouping type rules

---
 ex/HoTT book/Ch1.thy | 3 +--
 ex/Methods.thy       | 3 +--
 ex/Synthesis.thy     | 7 +++----
 3 files changed, 5 insertions(+), 8 deletions(-)

(limited to 'ex')

diff --git a/ex/HoTT book/Ch1.thy b/ex/HoTT book/Ch1.thy
index cc0adf5..d5f05dd 100644
--- a/ex/HoTT book/Ch1.thy	
+++ b/ex/HoTT book/Ch1.thy	
@@ -1,6 +1,5 @@
 (*  Title:  HoTT/ex/HoTT book/Ch1.thy
     Author: Josh Chen
-    Date:   Aug 2018
 
 A formalization of some content of Chapter 1 of the Homotopy Type Theory book.
 *)
@@ -41,4 +40,4 @@ proof (rule Sum_elim[where ?p=p])
 qed (derive lems: assms)
 
 
-end
\ No newline at end of file
+end
diff --git a/ex/Methods.thy b/ex/Methods.thy
index 871964f..415fbc3 100644
--- a/ex/Methods.thy
+++ b/ex/Methods.thy
@@ -1,6 +1,5 @@
 (*  Title:  HoTT/ex/Methods.thy
     Author: Josh Chen
-    Date:   Aug 2018
 
 HoTT method usage examples
 *)
@@ -74,4 +73,4 @@ proof compute
 qed fact
 
 
-end
\ No newline at end of file
+end
diff --git a/ex/Synthesis.thy b/ex/Synthesis.thy
index e5a8ecf..cff9374 100644
--- a/ex/Synthesis.thy
+++ b/ex/Synthesis.thy
@@ -1,6 +1,5 @@
 (*  Title:  HoTT/ex/Synthesis.thy
     Author: Josh Chen
-    Date:   Aug 2018
 
 Examples of synthesis.
 *)
@@ -33,8 +32,8 @@ text "
 schematic_goal "?p`0 \<equiv> 0" and "\<And>n. n: \<nat> \<Longrightarrow> (?p`(succ n)) \<equiv> n"
 apply compute
 prefer 4 apply compute
-prefer 3 apply (rule Nat_rules)
-apply (rule Nat_rules | assumption)+
+prefer 3 apply compute
+apply (rule Nat_routine Nat_elim | assumption)+
 done
 
 text "
@@ -52,7 +51,7 @@ proof (simple lems: pred_type)
   proof compute
     show "\<And>n. n: \<nat> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>a b. a) 0 n: \<nat>" by simple
     show "ind\<^sub>\<nat> (\<lambda>a b. a) 0 0 \<equiv> 0"
-    proof (rule Nat_comps)
+    proof compute
       show "\<nat>: U(O)" ..
     qed simple
   qed rule
-- 
cgit v1.2.3