1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory AutoLevity_Test
8imports
9  Lib.AutoLevity_Base
10  Lib.AutoLevity_Hooks
11begin
12locale foo = fixes z assumes Z:"z" begin
13ML \<open>Method.finish_text\<close>
14lemma
15X:
16"(z \<and> z) \<and> (z \<and> z)"
17apply (insert mp) apply (insert conjE)
18apply (rule conjI)
19subgoal
20  apply (rule
21conjI)
22  by
23(rule
24Z)
25(rule
26
27Z)
28subgoal apply (rule conjI)
29  subgoal
30    subgoal
31      subgoal apply (insert impE) by (rule
32Z)
33      done
34   done
35   proof -
36    show "z"
37      apply
38(rule
39 Z)
40      done
41   qed
42done
43
44end
45
46interpretation foo "True" by (unfold_locales;
47simp)
48
49
50
51end
52