Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/nominal_mutual.ML
changeset 3226 780b7a2c50b6
parent 3219 e5d9b6bca88c
child 3227 35bb5b013f0e
equal deleted inserted replaced
3225:b7b80d5640bb 3226:780b7a2c50b6 
   333 
   333 
   334     val induct_thm = case induct_thms of
 
   334     val induct_thm = case induct_thms of
 
   335         [thm] => thm
 
   335         [thm] => thm
 
   336           |> Drule.gen_all 
   336           |> Drule.gen_all 
   337           |> Thm.permute_prems 0 1
 
   337           |> Thm.permute_prems 0 1
 
   338           |> (fn thm => atomize_rule (length (prems_of thm) - 1) thm)
 
   338           |> (fn thm => atomize_rule ctxt' (length (prems_of thm) - 1) thm)
 
   339       | thms => thms
 
   339       | thms => thms
 
   340           |> map Drule.gen_all 
   340           |> map Drule.gen_all 
   341           |> map (Rule_Cases.add_consumes 1)
 
   341           |> map (Rule_Cases.add_consumes 1)
 
   342           |> snd o Rule_Cases.strict_mutual_rule ctxt'
 
   342           |> snd o Rule_Cases.strict_mutual_rule ctxt'
 
   343           |> atomize_concl
 
   343           |> atomize_concl ctxt'
 
   344 
   344 
   345     fun tac thm = rtac (Drule.gen_all thm) THEN_ALL_NEW atac
 
   345     fun tac thm = rtac (Drule.gen_all thm) THEN_ALL_NEW atac
 
   346   in
 
   346   in
 
   347     Goal.prove ctxt' (flat arg_namess) [] goal
 
   347     Goal.prove ctxt' (flat arg_namess) [] goal
 
   348       (fn {context, ...} => HEADGOAL (DETERM o (rtac induct_thm) THEN' RANGE (map tac eqvts_thms)))
 
   348       (fn {context, ...} => HEADGOAL (DETERM o (rtac induct_thm) THEN' RANGE (map tac eqvts_thms)))
nominal2