equal
deleted
inserted
replaced
1 (* Title: HOL/Record.thy |
1 (* Title: HOL/Record.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen |
3 Author: Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 theory Record = Product_Type |
6 theory Record |
7 files ("Tools/record_package.ML"): |
7 import Product_Type |
|
8 files ("Tools/record_package.ML") |
|
9 begin |
8 |
10 |
9 ML {* |
11 ML {* |
10 val [h1, h2] = Goal "PROP Goal (\<And>x. PROP P x) \<Longrightarrow> (PROP P x \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q"; |
12 val [h1, h2] = Goal "PROP Goal (\<And>x. PROP P x) \<Longrightarrow> (PROP P x \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q"; |
11 by (rtac h2 1); |
13 by (rtac h2 1); |
12 by (rtac (gen_all (h1 RS Drule.rev_triv_goal)) 1); |
14 by (rtac (gen_all (h1 RS Drule.rev_triv_goal)) 1); |