equal
deleted
inserted
replaced
45 let |
45 let |
46 val ops = map (fst o Term.strip_comb) ts; |
46 val ops = map (fst o Term.strip_comb) ts; |
47 fun ord (Const (a, _)) = find_index (fn (Const (b, _)) => a=b | _ => false) ops |
47 fun ord (Const (a, _)) = find_index (fn (Const (b, _)) => a=b | _ => false) ops |
48 | ord (Free (a, _)) = find_index (fn (Free (b, _)) => a=b | _ => false) ops; |
48 | ord (Free (a, _)) = find_index (fn (Free (b, _)) => a=b | _ => false) ops; |
49 fun less (a, b) = (Term_Ord.term_lpo ord (a, b) = LESS); |
49 fun less (a, b) = (Term_Ord.term_lpo ord (a, b) = LESS); |
50 in asm_full_simp_tac (HOL_ss settermless less addsimps simps) end; |
50 in asm_full_simp_tac (HOL_ss addsimps simps |> Simplifier.set_termless less) end; |
51 |
51 |
52 fun algebra_tac ctxt = |
52 fun algebra_tac ctxt = |
53 EVERY' (map (fn s => TRY o struct_tac s) (Data.get (Context.Proof ctxt))); |
53 EVERY' (map (fn s => TRY o struct_tac s) (Data.get (Context.Proof ctxt))); |
54 |
54 |
55 |
55 |