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