1(*
2 * Copyright 2014, NICTA
3 *
4 * This software may be distributed and modified according to the terms of
5 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
6 * See "LICENSE_BSD2.txt" for details.
7 *
8 * @TAG(NICTA_BSD)
9 *
10 *)
11
12theory AutoLevity_Test
13imports
14  Lib.AutoLevity_Base
15  Lib.AutoLevity_Hooks
16begin
17locale foo = fixes z assumes Z:"z" begin
18ML \<open>Method.finish_text\<close>
19lemma
20X:
21"(z \<and> z) \<and> (z \<and> z)"
22apply (insert mp) apply (insert conjE)
23apply (rule conjI)
24subgoal
25  apply (rule
26conjI)
27  by
28(rule
29Z)
30(rule
31
32Z)
33subgoal apply (rule conjI)
34  subgoal
35    subgoal
36      subgoal apply (insert impE) by (rule
37Z)
38      done
39   done
40   proof -
41    show "z"
42      apply
43(rule
44 Z)
45      done
46   qed
47done
48
49end
50
51interpretation foo "True" by (unfold_locales;
52simp)
53
54
55
56end
57