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