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/Synthesis.thy | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'ex/Synthesis.thy')

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