diff options
| author | Josh Chen | 2018-08-18 23:27:25 +0200 |
|---|---|---|
| committer | Josh Chen | 2018-08-18 23:27:25 +0200 |
| commit | 8833cdf99d3128466d85eb88aeb8e340e07e937c (patch) | |
| tree | 87094caffe667540ac03cc05e9e1054c04a112d9 /tests | |
| parent | e1be5f97bb2a42b3179bc24b118d69af137f8e5d (diff) | |
Reorganize methods
Diffstat (limited to '')
| -rw-r--r-- | tests/Subgoal.thy | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/tests/Subgoal.thy b/tests/Subgoal.thy index 9690013..82d7e5d 100644 --- a/tests/Subgoal.thy +++ b/tests/Subgoal.thy @@ -25,11 +25,11 @@ apply standard apply (rule Prod_intro) subgoal premises 4 for u z q apply (rule Equal_elim[where ?x=u and ?y=z]) - apply (simple lems: assms 4) + apply (routine lems: assms 4) done - apply (simple lems: assms 1 2 3) + apply (routine lems: assms 1 2 3) done - apply (simple lems: assms 1 2) + apply (routine lems: assms 1 2) done apply fact done @@ -52,9 +52,9 @@ text " Try (and fail) to synthesize the constant for path composition, following the proof of \<open>rpathcomp_type\<close> below. " -apply (rule Prod_intro) - apply (rule Prod_intro) - apply (rule Prod_intro) +apply (rule intros) + apply (rule intros) + apply (rule intros) subgoal 123 for x y p apply (rule Equal_elim[where ?x=x and ?y=y and ?A=A]) oops |