From 2f0da5f6ba29955f642f8de0be7c3de75ce6e6f1 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Tue, 27 Dec 2016 10:50:50 +0000 Subject: [PATCH] Removed sorry's. --- FWNormalisation/NormalisationIntegerPortProof.thy | 2 -- 1 file changed, 2 deletions(-) diff --git a/FWNormalisation/NormalisationIntegerPortProof.thy b/FWNormalisation/NormalisationIntegerPortProof.thy index 7d7d944..8c104a7 100644 --- a/FWNormalisation/NormalisationIntegerPortProof.thy +++ b/FWNormalisation/NormalisationIntegerPortProof.thy @@ -609,8 +609,6 @@ lemma rule_charn2: case Nil show ?case using Nil by simp next case (snoc y ys) - then have * : " y = AllowPortFromTo c d po \ ys \ []" sorry - have ** : "applied_rule_rev C x ys = Some (AllowPortFromTo c d po)" sledgehammer sorry show ?case using snoc apply (case_tac "y = (AllowPortFromTo c d po)", simp_all ) apply (simp add: applied_rule_rev_def)